let d, e be Nat; :: thesis: for p being Prime st p > 2 & d gcd p = 1 & e gcd p = 1 holds
Lege (((d ^2) * e),p) = Lege (e,p)
let p be Prime; :: thesis: ( p > 2 & d gcd p = 1 & e gcd p = 1 implies Lege (((d ^2) * e),p) = Lege (e,p) )
assume that
A1: p > 2 and
A2: d gcd p = 1 and
A3: e gcd p = 1 ; :: thesis: Lege (((d ^2) * e),p) = Lege (e,p)
reconsider d2 = d ^2 , e = e as Element of NAT by ORDINAL1:def 12;
set fp = <*d2,e*>;
reconsider fp = <*d2,e*> as FinSequence of NAT by FINSEQ_2:13;
not p divides d by A2, Lm3;
then d mod p <> 0 by INT_1:62;
then A4: Lege ((d ^2),p) = 1 by Th26;
reconsider p = p as prime Element of NAT by ORDINAL1:def 12;
for k being Nat st k in dom fp holds
(fp . k) gcd p = 1

proof

let k be Nat; :: thesis: ( k in dom fp implies (fp . k) gcd p = 1 )
assume k in dom fp ; :: thesis: (fp . k) gcd p = 1
then k in Seg (len fp) by FINSEQ_1:def 3;
then A5: k in Seg 2 by FINSEQ_1:44;

per cases ( k = 1 or k = 2 ) by A5, FINSEQ_1:2, TARSKI:def 2;

suppose k = 1 ; :: thesis: (fp . k) gcd p = 1

then fp . k = d ^2 ;
hence (fp . k) gcd p = 1 by A2, WSIERP_1:7; :: thesis: verum

end;

suppose k = 2 ; :: thesis: (fp . k) gcd p = 1

hence (fp . k) gcd p = 1 by A3; :: thesis: verum

end;

end;

end;

then consider fr being FinSequence of INT such that
A6: len fr = len fp and
A7: for k being Nat st k in dom fr holds
fr . k = Lege ((fp . k),p) and
A8: Lege ((Product fp),p) = Product fr by A1, Th34;
A9: len fr = 2 by A6, FINSEQ_1:44;
then 2 in dom fr by FINSEQ_3:25;
then fr . 2 = Lege ((fp . 2),p) by A7;
then A10: fr . 2 = Lege (e,p) ;
fr . 1 = Lege ((fp . 1),p) by A7, A9, FINSEQ_3:25;
then fr . 1 = Lege ((d ^2),p) ;
then fr = <*1,(Lege (e,p))*> by A4, A9, A10, FINSEQ_1:44;
then Product fr = 1 * (Lege (e,p)) by RVSUM_1:99;
hence Lege (((d ^2) * e),p) = Lege (e,p) by A8, RVSUM_1:99; :: thesis: verum