let z be Complex; :: thesis: for k being Nat holds
( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k )
let k be Nat; :: thesis: ( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k )
defpred S₁[ Nat] means ( z |^ (2 * $1) = (z |^ $1) |^ 2 & z |^ (2 * $1) = (z |^ 2) |^ $1 );
A1: z |^ (2 * 0) = 1 * 1 by NEWTON:4
.= (1 |^ 1) * 1 by NEWTON:5
.= 1 |^ (1 + 1) by NEWTON:6
.= (z |^ 0) |^ 2 by NEWTON:4 ;
z |^ (2 * 0) = 1 by NEWTON:4
.= (z |^ 2) |^ 0 by NEWTON:4 ;
then A2: S₁[ 0 ] by A1;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A4: z |^ (2 * k) = (z |^ k) |^ 2 and
A5: z |^ (2 * k) = (z |^ 2) |^ k ; :: thesis: S₁[k + 1]
A6: z |^ (2 * (k + 1)) = (z GeoSeq) . (((2 * k) + 1) + 1)
.= ((z GeoSeq) . ((2 * k) + 1)) * z by COMSEQ_3:def 1
.= ((z |^ (2 * k)) * z) * z by COMSEQ_3:def 1 ;
then A7: z |^ (2 * (k + 1)) = ((((z |^ k) GeoSeq) . (1 + 1)) * z) * z by A4
.= (((((z |^ k) GeoSeq) . (0 + 1)) * (z |^ k)) * z) * z by COMSEQ_3:def 1
.= ((((((z |^ k) GeoSeq) . 0) * (z |^ k)) * (z |^ k)) * z) * z by COMSEQ_3:def 1
.= (((1r * (z |^ k)) * (z |^ k)) * z) * z by COMSEQ_3:def 1
.= (1r * (((z GeoSeq) . k) * z)) * ((z |^ k) * z)
.= (1r * ((z GeoSeq) . (k + 1))) * (((z GeoSeq) . k) * z) by COMSEQ_3:def 1
.= (1r * (z |^ (k + 1))) * ((z GeoSeq) . (k + 1)) by COMSEQ_3:def 1
.= ((((z |^ (k + 1)) GeoSeq) . 0) * (z |^ (k + 1))) * (z |^ (k + 1)) by COMSEQ_3:def 1
.= (((z |^ (k + 1)) GeoSeq) . (0 + 1)) * (z |^ (k + 1)) by COMSEQ_3:def 1
.= ((z |^ (k + 1)) GeoSeq) . ((0 + 1) + 1) by COMSEQ_3:def 1
.= (z |^ (k + 1)) |^ 2 ;
z |^ (2 * (k + 1)) = ((z |^ 2) |^ k) * ((1r * z) * z) by A5, A6
.= ((z |^ 2) |^ k) * ((((z GeoSeq) . 0) * z) * z) by COMSEQ_3:def 1
.= ((z |^ 2) |^ k) * (((z GeoSeq) . (0 + 1)) * z) by COMSEQ_3:def 1
.= ((z |^ 2) |^ k) * ((z GeoSeq) . ((0 + 1) + 1)) by COMSEQ_3:def 1
.= (z |^ 2) |^ (k + 1) by COMSEQ_3:def 1 ;
hence S₁[k + 1] by A7; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence ( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k ) ; :: thesis: verum