let R be Ring; :: thesis: for V1, V2 being LeftMod of R

for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

let V1, V2 be LeftMod of R; :: thesis: for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

let f be Function of V1,V2; :: thesis: for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

let p be FinSequence of V1; :: thesis: ( f is additive & f is homogeneous implies f . (Sum p) = Sum (f * p) )

defpred S_{1}[ FinSequence of V1] means f . (Sum $1) = Sum (f * $1);

assume A1: ( f is additive & f is homogeneous ) ; :: thesis: f . (Sum p) = Sum (f * p)

A2: for p being FinSequence of V1

for w being Element of V1 st S_{1}[p] holds

S_{1}[p ^ <*w*>]

.= f . ((0. R) * (0. V1)) by VECTSP_1:14

.= (0. R) * (f . (0. V1)) by A1

.= 0. V2 by VECTSP_1:14

.= Sum (<*> the carrier of V2) by RLVECT_1:43

.= Sum (f * (<*> the carrier of V1)) ;

then A4: S_{1}[ <*> the carrier of V1]
;

for p being FinSequence of V1 holds S_{1}[p]
from FINSEQ_2:sch 2(A4, A2);

hence f . (Sum p) = Sum (f * p) ; :: thesis: verum

for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

let V1, V2 be LeftMod of R; :: thesis: for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

let f be Function of V1,V2; :: thesis: for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

let p be FinSequence of V1; :: thesis: ( f is additive & f is homogeneous implies f . (Sum p) = Sum (f * p) )

defpred S

assume A1: ( f is additive & f is homogeneous ) ; :: thesis: f . (Sum p) = Sum (f * p)

A2: for p being FinSequence of V1

for w being Element of V1 st S

S

proof

f . (Sum (<*> the carrier of V1)) =
f . (0. V1)
by RLVECT_1:43
let p be FinSequence of V1; :: thesis: for w being Element of V1 st S_{1}[p] holds

S_{1}[p ^ <*w*>]

let w be Element of V1; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*w*>] )

assume A3: f . (Sum p) = Sum (f * p) ; :: thesis: S_{1}[p ^ <*w*>]

thus f . (Sum (p ^ <*w*>)) = f . ((Sum p) + (Sum <*w*>)) by RLVECT_1:41

.= (Sum (f * p)) + (f . (Sum <*w*>)) by A1, A3

.= (Sum (f * p)) + (f . w) by RLVECT_1:44

.= (Sum (f * p)) + (Sum <*(f . w)*>) by RLVECT_1:44

.= Sum ((f * p) ^ <*(f . w)*>) by RLVECT_1:41

.= Sum (f * (p ^ <*w*>)) by FINSEQOP:8 ; :: thesis: verum

end;S

let w be Element of V1; :: thesis: ( S

assume A3: f . (Sum p) = Sum (f * p) ; :: thesis: S

thus f . (Sum (p ^ <*w*>)) = f . ((Sum p) + (Sum <*w*>)) by RLVECT_1:41

.= (Sum (f * p)) + (f . (Sum <*w*>)) by A1, A3

.= (Sum (f * p)) + (f . w) by RLVECT_1:44

.= (Sum (f * p)) + (Sum <*(f . w)*>) by RLVECT_1:44

.= Sum ((f * p) ^ <*(f . w)*>) by RLVECT_1:41

.= Sum (f * (p ^ <*w*>)) by FINSEQOP:8 ; :: thesis: verum

.= f . ((0. R) * (0. V1)) by VECTSP_1:14

.= (0. R) * (f . (0. V1)) by A1

.= 0. V2 by VECTSP_1:14

.= Sum (<*> the carrier of V2) by RLVECT_1:43

.= Sum (f * (<*> the carrier of V1)) ;

then A4: S

for p being FinSequence of V1 holds S

hence f . (Sum p) = Sum (f * p) ; :: thesis: verum