let X be Banach_Algebra; :: thesis: for n being Element of 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 Element of 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₁[ Element of NAT ] means ( w * (z #N $1) = (z #N $1) * w & z * (w #N $1) = (w #N $1) * z );
A2: z #N 0 = 1. X by LOPBAN_3:def 13;
A3: w #N 0 = 1. X by LOPBAN_3:def 13;
A4: w * (z #N 0 ) = w by A2, LOPBAN_3:43
.= (z #N 0 ) * w by A2, LOPBAN_3:43 ;
z * (w #N 0 ) = z by A3, LOPBAN_3:43
.= (w #N 0 ) * z by A3, LOPBAN_3:43 ;
then A5: S₁[ 0 ] by A4;
A6: 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 A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: w * (z #N (k + 1)) = w * ((z #N k) * z) by Lm1
.= (w * (z #N k)) * z by LOPBAN_3:43
.= (z #N k) * (w * z) by A7, LOPBAN_3:43
.= (z #N k) * (z * w) by A1, Def1
.= ((z #N k) * z) * w by LOPBAN_3:43
.= (z #N (k + 1)) * w by Lm1 ;
z * (w #N (k + 1)) = z * ((w #N k) * w) by Lm1
.= (z * (w #N k)) * w by LOPBAN_3:43
.= (w #N k) * (z * w) by A7, LOPBAN_3:43
.= (w #N k) * (w * z) by A1, Def1
.= ((w #N k) * w) * z by LOPBAN_3:43
.= (w #N (k + 1)) * z by Lm1 ;
hence S₁[k + 1] by A8; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A6);
hence ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) ; :: thesis: verum