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

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

Partial_Sums (z * seq) = z * (Partial_Sums seq)
defpred S_{1}[ Nat] means (Partial_Sums (seq * z)) . $1 = ((Partial_Sums seq) * z) . $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: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A2);

then for n being Element of NAT holds S_{1}[n]
;

hence Partial_Sums (seq * z) = (Partial_Sums seq) * z by FUNCT_2:63; :: thesis: verum

end;A2: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

(Partial_Sums (seq * z)) . 0 =
(seq * z) . 0
by BHSP_4:def 1
S

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[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 A3, LOPBAN_3:def 6

.= (((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 S_{1}[n + 1]
; :: thesis: verum

end;assume A3: S

(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 A3, LOPBAN_3:def 6

.= (((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 S

.= (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: S

for n being Nat holds S

then for n being Element of NAT holds S

hence Partial_Sums (seq * z) = (Partial_Sums seq) * z by FUNCT_2:63; :: thesis: verum

proof

hence
( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z )
by A1; :: thesis: verum
defpred S_{1}[ Nat] means (Partial_Sums (z * seq)) . $1 = (z * (Partial_Sums seq)) . $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: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A7, A5);

then for n being Element of NAT holds S_{1}[n]
;

hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by FUNCT_2:63; :: thesis: verum

end;A5: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

(Partial_Sums (z * seq)) . 0 =
(z * seq) . 0
by BHSP_4:def 1
S

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A6: S_{1}[n]
; :: thesis: S_{1}[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 A6, LOPBAN_3:def 5

.= (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 S_{1}[n + 1]
; :: thesis: verum

end;assume A6: S

(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 A6, LOPBAN_3:def 5

.= (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 S

.= 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: S

for n being Nat holds S

then for n being Element of NAT holds S

hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by FUNCT_2:63; :: thesis: verum