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 13;
set fp = <*d2,e*>;
reconsider fp = <*d2,e*> as FinSequence of NAT by FINSEQ_2:15;
A4: Lege (d ^2 ),p = 1 by Th26;
reconsider p = p as prime Element of NAT by ORDINAL1:def 13;
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:61;

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

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

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

end;

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

hence (fp . k) gcd p = 1 by A3, FINSEQ_1:61; :: 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:61;
then 2 in dom fr by FINSEQ_3:27;
then fr . 2 = Lege (fp . 2),p by A7;
then A10: fr . 2 = Lege e,p by FINSEQ_1:61;
1 in dom fr by A9, FINSEQ_3:27;
then fr . 1 = Lege (fp . 1),p by A7;
then fr . 1 = Lege (d ^2 ),p by FINSEQ_1:61;
then fr = <*1,(Lege e,p)*> by A4, A9, A10, FINSEQ_1:61;
then Product fr = 1 * (Lege e,p) by RVSUM_1:129;
hence Lege ((d ^2 ) * e),p = Lege e,p by A8, RVSUM_1:129; :: thesis: verum