let X be Complex_Banach_Algebra; :: thesis: for z being Element of X
for n being Element of NAT holds
( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z )
let z be Element of X; :: thesis: for n being Element of NAT holds
( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z )
let n be Element of NAT ; :: thesis: ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z )
defpred S₁[ Element of NAT ] means z * (z #N $1) = z #N ($1 + 1);
A1: z * (z #N 0 ) = z * ((z GeoSeq ) . 0 ) by CLOPBAN3:def 13
.= z * (1. X) by CLOPBAN3:def 12
.= z by CLOPBAN3:42 ;
z #N (0 + 1) = (z GeoSeq ) . (0 + 1) by CLOPBAN3:def 13
.= ((z GeoSeq ) . 0 ) * z by CLOPBAN3:def 12
.= (1. X) * z by CLOPBAN3:def 12
.= z by CLOPBAN3:42 ;
then A2: S₁[ 0 ] by A1;
A3: 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 A4: S₁[k] ; :: thesis: S₁[k + 1]
thus z * (z #N (k + 1)) = z * ((z GeoSeq ) . (k + 1)) by CLOPBAN3:def 13
.= z * (((z GeoSeq ) . k) * z) by CLOPBAN3:def 12
.= z * ((z #N k) * z) by CLOPBAN3:def 13
.= (z * (z #N k)) * z by CLOPBAN3:42
.= ((z GeoSeq ) . (k + 1)) * z by A4, CLOPBAN3:def 13
.= (z GeoSeq ) . ((k + 1) + 1) by CLOPBAN3:def 12
.= z #N ((k + 1) + 1) by CLOPBAN3:def 13 ; :: thesis: verum

end;

A5: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);

now

let n be Element of NAT ; :: thesis: ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z )
thus z * (z #N n) = z #N (n + 1) by A5; :: thesis: ( (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z )
thus (z #N n) * z = ((z GeoSeq ) . n) * z by CLOPBAN3:def 13
.= (z GeoSeq ) . (n + 1) by CLOPBAN3:def 12
.= z #N (n + 1) by CLOPBAN3:def 13 ; :: thesis: z * (z #N n) = (z #N n) * z
hence z * (z #N n) = (z #N n) * z by A5; :: thesis: verum

end;

hence ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) ; :: thesis: verum