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 A1: ( p > 2 & d gcd p = 1 & e gcd p = 1 ) ; :: thesis: Lege ((d ^2 ) * e),p = Lege e,p
then A2: Lege (d ^2 ),p = 1 by Th26;
reconsider d2 = d ^2 , e = e as Element of NAT by ORDINAL1:def 13;
set fp = <*d2,e*>;
reconsider p = p as prime Element of NAT by ORDINAL1:def 13;
reconsider fp = <*d2,e*> as FinSequence of NAT by FINSEQ_2:15;
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 A3: k in Seg 2 by FINSEQ_1:61;

per cases ( k = 1 or k = 2 ) by A3, 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 A1, WSIERP_1:12; :: thesis: verum

end;

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

hence (fp . k) gcd p = 1 by A1, FINSEQ_1:61; :: thesis: verum

end;

end;

end;

then consider fr being FinSequence of INT such that
A5: ( len fr = len fp & ( for k being Nat st k in dom fr holds
fr . k = Lege (fp . k),p ) & Lege (Product fp),p = Product fr ) by A1, Th34;
A6: len fr = 2 by A5, FINSEQ_1:61;
then ( 1 in dom fr & 2 in dom fr ) by FINSEQ_3:27;
then ( fr . 1 = Lege (fp . 1),p & fr . 2 = Lege (fp . 2),p ) by A5;
then ( fr . 1 = Lege (d ^2 ),p & fr . 2 = Lege e,p ) by FINSEQ_1:61;
then fr = <*1,(Lege e,p)*> by A2, A6, FINSEQ_1:61;
then Product fr = 1 * (Lege e,p) by RVSUM_1:129;
hence Lege ((d ^2 ) * e),p = Lege e,p by A5, RVSUM_1:129; :: thesis: verum