let X be Complex_Banach_Algebra; 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; 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; ( 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
; ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z )
defpred S1[ Nat] means ( w * (z #N $1) = (z #N $1) * w & z * (w #N $1) = (w #N $1) * z );
A2:
for k being Nat st S1[k] holds
S1[k + 1]
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:
S1[ 0 ]
by A6;
for n being Nat holds S1[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 )
; verum