let p be 2 _greater Prime; :: thesis: for a, b being Integer st a gcd p = 1 & b gcd p = 1 & a,b are_congruent_mod p holds
Leg (a,p) = Leg (b,p)
let a, b be Integer; :: thesis: ( a gcd p = 1 & b gcd p = 1 & a,b are_congruent_mod p implies Leg (a,p) = Leg (b,p) )
assume A1: ( a gcd p = 1 & b gcd p = 1 & a,b are_congruent_mod p ) ; :: thesis: Leg (a,p) = Leg (b,p)
thus Leg (a,p) = Lege (a,p) by Lm4
.= Lege (b,p) by Def1, A1, INT_5:29
.= Leg (b,p) by Lm4 ; :: thesis: verum