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 (seq * z) = (Partial_Sums seq) * z
proof
defpred S1[ Nat] means (Partial_Sums (seq * z)) . \$1 = ((Partial_Sums seq) * z) . \$1;
A2: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
(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
.= (((Partial_Sums seq) . n) * z) + ((seq . (n + 1)) * z) by LOPBAN_3:def 6
.= (((Partial_Sums seq) . n) + (seq . (n + 1))) * z by VECTSP_1:def 3
.= ((Partial_Sums seq) . (n + 1)) * z by BHSP_4:def 1
.= ((Partial_Sums seq) * z) . (n + 1) by LOPBAN_3:def 6 ;
hence S1[n + 1] ; :: thesis: verum
end;
(Partial_Sums (seq * z)) . 0 = (seq * z) . 0 by BHSP_4:def 1
.= (seq . 0) * z by LOPBAN_3:def 6
.= ((Partial_Sums seq) . 0) * z by BHSP_4:def 1
.= ((Partial_Sums seq) * z) . 0 by LOPBAN_3:def 6 ;
then A4: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A2);
then for n being Element of NAT holds S1[n] ;
hence Partial_Sums (seq * z) = (Partial_Sums seq) * z by FUNCT_2:63; :: thesis: verum
end;
Partial_Sums (z * seq) = z * (Partial_Sums seq)
proof
defpred S1[ Nat] means (Partial_Sums (z * seq)) . \$1 = (z * (Partial_Sums seq)) . \$1;
A5: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; :: thesis: S1[n + 1]
(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
.= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by LOPBAN_3:def 5
.= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by VECTSP_1:def 2
.= z * ((Partial_Sums seq) . (n + 1)) by BHSP_4:def 1
.= (z * (Partial_Sums seq)) . (n + 1) by LOPBAN_3:def 5 ;
hence S1[n + 1] ; :: thesis: verum
end;
(Partial_Sums (z * seq)) . 0 = (z * seq) . 0 by BHSP_4:def 1
.= z * (seq . 0) by LOPBAN_3:def 5
.= z * ((Partial_Sums seq) . 0) by BHSP_4:def 1
.= (z * (Partial_Sums seq)) . 0 by LOPBAN_3:def 5 ;
then A7: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A7, A5);
then for n being Element of NAT holds S1[n] ;
hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by FUNCT_2:63; :: thesis: verum
end;
hence ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) by A1; :: thesis: verum