Dokažimo sada da uslov y=faktorijel(z) jeste invarijanta petlje polaznog programa za proizvoljan ulaz. Ono što treba da dokažemo je da svaki put kada se ulazi u petlju važi dati uslov.
Dokaz se sastoji iz tri koraka:
1. Uspostavljanje invarijante. Najpre treba da dokažemo da prvi put kada naiđemo na ulazak u petlju važi uslov y=faktorijel(z). To je ispunjeno, jer pre prvog ulaska u petlju postoje dve naredbe dodele (y dobija vrednost 1 i z dobija vrednost 0), a važi da je 1=faktorijel(0).
2. Održavanje invarijante. Dalje treba da dokažemo sledeće: ako uslov y=faktorijel(z) važi pre nekog ulaska u petlju, onda važi i nakon (jednog) izvršavanja tela petlje. Označimo sa y' vrednost promenljive y nakon izvršavanja odgovarajuće iteracije, a sa z' vrednost promenljive z nakon izvršavanja te iste iteracije. Tada tvrđenje važi na osnovu sledećih jednakosti:
y' = y * z' = y * (z + 1) = faktorijel(z) * (z + 1)=
= faktorijel(z + 1) = faktorijel(z')
Za treću jednakost korišćena je pretpostavka da invarijanta važi pre iteracije (tj. da važi y=faktorijel(z)), a za četvrtu jednakost korišćena je definicija faktorijela.
Primetimo da je ovaj dokaz u suštini induktivne prirode.
Ovim smo dokazali da svaki put kada se ispituje uslov ulaska u petlju, važi da je uslov y=faktorijel(z) ispunjen.
3. Ostvarivanje željenog pauslova. Na kraju, ako se izvršavanje petlje okonča (tj. ako vrednost uslova ulaska u petlju postane netačna), tada je z=x, program se zaustavlja i važi da je y=faktorijel(x).