let X be Complex_Banach_Algebra; :: thesis: for n being Nat
for z, w being Element of X st z,w are_commutative holds
( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z )
let n be Nat; :: thesis: for z, w being Element of X st z,w are_commutative holds
( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z )
let z, w be Element of X; :: thesis: ( z,w are_commutative implies ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) )
assume A1: z,w are_commutative ; :: thesis: ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z )
defpred S₁[ Nat] means ( w * (z #N $1) = (z #N $1) * w & z * (w #N $1) = (w #N $1) * z );
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: z * (w #N (k + 1)) = z * ((w #N k) * w) by Lm1
.= (z * (w #N k)) * w by GROUP_1:def 3
.= (w #N k) * (z * w) by A3, GROUP_1:def 3
.= (w #N k) * (w * z) by A1, LOPBAN_4:def 1
.= ((w #N k) * w) * z by GROUP_1:def 3
.= (w #N (k + 1)) * z by Lm1 ;
w * (z #N (k + 1)) = w * ((z #N k) * z) by Lm1
.= (w * (z #N k)) * z by GROUP_1:def 3
.= (z #N k) * (w * z) by A3, GROUP_1:def 3
.= (z #N k) * (z * w) by A1, LOPBAN_4:def 1
.= ((z #N k) * z) * w by GROUP_1:def 3
.= (z #N (k + 1)) * w by Lm1 ;
hence S₁[k + 1] by A4; :: thesis: verum

end;

A5: w #N 0 = (w GeoSeq) . 0 by CLOPBAN3:def 8
.= 1. X by CLOPBAN3:def 7 ;
then A6: z * (w #N 0) = z by VECTSP_1:def 4
.= (w #N 0) * z by A5, VECTSP_1:def 8 ;
A7: z #N 0 = (z GeoSeq) . 0 by CLOPBAN3:def 8
.= 1. X by CLOPBAN3:def 7 ;
then w * (z #N 0) = w by VECTSP_1:def 4
.= (z #N 0) * w by A7, VECTSP_1:def 8 ;
then A8: S₁[ 0 ] by A6;
for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A2);
hence ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) ; :: thesis: verum