let X be Complex_Banach_Algebra; :: thesis: for z being Element of X
for seq being sequence of X holds
( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z )
let z be Element of X; :: thesis: for seq being sequence of X holds
( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z )
let seq be sequence of X; :: thesis: ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z )
A1: Partial_Sums (z * seq) = z * (Partial_Sums seq)

proof

defpred S₁[ Element of NAT ] means (Partial_Sums (z * seq)) . $1 = (z * (Partial_Sums seq)) . $1;
A2: S₁[ 0 ]

proof

thus (Partial_Sums (z * seq)) . 0 = (z * seq) . 0 by BHSP_4:def 1
.= z * (seq . 0 ) by CLOPBAN3:def 8
.= z * ((Partial_Sums seq) . 0 ) by BHSP_4:def 1
.= (z * (Partial_Sums seq)) . 0 by CLOPBAN3:def 8 ; :: thesis: verum

end;

A3: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

thus (Partial_Sums (z * seq)) . (n + 1) = ((Partial_Sums (z * seq)) . n) + ((z * seq) . (n + 1)) by BHSP_4:def 1
.= (z * ((Partial_Sums seq) . n)) + ((z * seq) . (n + 1)) by A4, CLOPBAN3:def 8
.= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by CLOPBAN3:def 8
.= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by CLOPBAN3:42
.= z * ((Partial_Sums seq) . (n + 1)) by BHSP_4:def 1
.= (z * (Partial_Sums seq)) . (n + 1) by CLOPBAN3:def 8 ; :: thesis: verum

end;

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by FUNCT_2:113; :: thesis: verum

end;

Partial_Sums (seq * z) = (Partial_Sums seq) * z

proof

defpred S₁[ Element of NAT ] means (Partial_Sums (seq * z)) . $1 = ((Partial_Sums seq) * z) . $1;
A5: S₁[ 0 ]

proof

thus (Partial_Sums (seq * z)) . 0 = (seq * z) . 0 by BHSP_4:def 1
.= (seq . 0 ) * z by CLOPBAN3:def 9
.= ((Partial_Sums seq) . 0 ) * z by BHSP_4:def 1
.= ((Partial_Sums seq) * z) . 0 by CLOPBAN3:def 9 ; :: thesis: verum

end;

A6: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

thus (Partial_Sums (seq * z)) . (n + 1) = ((Partial_Sums (seq * z)) . n) + ((seq * z) . (n + 1)) by BHSP_4:def 1
.= (((Partial_Sums seq) . n) * z) + ((seq * z) . (n + 1)) by A7, CLOPBAN3:def 9
.= (((Partial_Sums seq) . n) * z) + ((seq . (n + 1)) * z) by CLOPBAN3:def 9
.= (((Partial_Sums seq) . n) + (seq . (n + 1))) * z by CLOPBAN3:42
.= ((Partial_Sums seq) . (n + 1)) * z by BHSP_4:def 1
.= ((Partial_Sums seq) * z) . (n + 1) by CLOPBAN3:def 9 ; :: thesis: verum

end;

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A6);
hence Partial_Sums (seq * z) = (Partial_Sums seq) * z by FUNCT_2:113; :: thesis: verum

end;

hence ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) by A1; :: thesis: verum