let p be natural prime 2 _greater number ; :: thesis: for a, b being integer number st a gcd p = 1 & b gcd p = 1 holds
Leg ((a * b),p) = (Leg (a,p)) * (Leg (b,p))
let a, b be integer number ; :: thesis: ( a gcd p = 1 & b gcd p = 1 implies Leg ((a * b),p) = (Leg (a,p)) * (Leg (b,p)) )
assume A1: ( a gcd p = 1 & b gcd p = 1 ) ; :: thesis: Leg ((a * b),p) = (Leg (a,p)) * (Leg (b,p))
thus Leg ((a * b),p) = Lege ((a * b),p) by Lm4
.= (Lege (a,p)) * (Lege (b,p)) by A1, Def1, INT_5:30
.= (Leg (a,p)) * (Lege (b,p)) by Lm4
.= (Leg (a,p)) * (Leg (b,p)) by Lm4 ; :: thesis: verum