let X be 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 LOPBAN_3:38
.= (w #N k) * (z * w) by A3, LOPBAN_3:38
.= (w #N k) * (w * z) by A1
.= ((w #N k) * w) * z by LOPBAN_3:38
.= (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 LOPBAN_3:38
.= (z #N k) * (w * z) by A3, LOPBAN_3:38
.= (z #N k) * (z * w) by A1
.= ((z #N k) * z) * w by LOPBAN_3:38
.= (z #N (k + 1)) * w by Lm1 ;
hence S₁[k + 1] by A4; :: thesis: verum

end;

A5: w #N 0 = 1. X by LOPBAN_3:def 9;
then A6: z * (w #N 0) = z by LOPBAN_3:38
.= (w #N 0) * z by A5, LOPBAN_3:38 ;
A7: z #N 0 = 1. X by LOPBAN_3:def 9;
then w * (z #N 0) = w by LOPBAN_3:38
.= (z #N 0) * w by A7, LOPBAN_3:38 ;
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