let p be natural prime 2 _greater number ; 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 ; ( 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 )
; 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
; verum