let n be natural non zero number ; :: thesis: for x being integer number
for k, l being natural number st k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n holds
k = l
let x be integer number ; :: thesis: for k, l being natural number st k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n holds
k = l
let k, l be natural number ; :: thesis: ( k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n implies k = l )
assume A1: ( k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n ) ; :: thesis: k = l
hence k = x mod n by Th12
.= l by A1, Th12 ;
:: thesis: verum