let z be complex number ; :: thesis: for k being Element of NAT holds
( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k )
let k be Element of NAT ; :: thesis: ( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k )
defpred S₁[ Element of NAT ] means ( z |^ (2 * $1) = (z |^ $1) |^ 2 & z |^ (2 * $1) = (z |^ 2) |^ $1 );
A1: z |^ (2 * 0 ) = 1 * 1 by NEWTON:9
.= (1 |^ 1) * 1 by NEWTON:10
.= 1 |^ (1 + 1) by NEWTON:11
.= (z |^ 0 ) |^ 2 by NEWTON:9 ;
A2: z |^ (2 * 0 ) = 1 by NEWTON:9
.= (z |^ 2) |^ 0 by NEWTON:9 ;
A3: S₁[ 0 ] by A1, A2;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A5: z |^ (2 * k) = (z |^ k) |^ 2 and
A6: z |^ (2 * k) = (z |^ 2) |^ k ; :: thesis: S₁[k + 1]
A7: 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 ;
A8: z |^ (2 * (k + 1)) = ((((z |^ k) GeoSeq ) . (1 + 1)) * z) * z by A5, A7
.= (((((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 ;
A9: z |^ (2 * (k + 1)) = ((z |^ 2) |^ k) * ((1r * z) * z) by A6, A7
.= ((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 ;
thus S₁[k + 1] by A8, A9; :: thesis: verum

end;

A10: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
thus ( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k ) by A10; :: thesis: verum