let K be Field; :: thesis: for V1, V2 being VectSp of K
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 VectSp of K; :: 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₁[ 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₁[p] holds
S₁[p ^ <*w*>]

proof

let p be FinSequence of V1; :: thesis: for w being Element of V1 st S₁[p] holds
S₁[p ^ <*w*>]
let w be Element of V1; :: thesis: ( S₁[p] implies S₁[p ^ <*w*>] )
assume A3: f . (Sum p) = Sum (f * p) ; :: thesis: S₁[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, VECTSP_1:def 20
.= (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;

f . (Sum (<*> the carrier of V1)) = f . (0. V1) by RLVECT_1:43
.= f . ((0. K) * (0. V1)) by VECTSP_1:14
.= (0. K) * (f . (0. V1)) by A1, MOD_2:def 2
.= 0. V2 by VECTSP_1:14
.= Sum (<*> the carrier of V2) by RLVECT_1:43
.= Sum (f * (<*> the carrier of V1)) ;
then A4: S₁[ <*> the carrier of V1] ;
for p being FinSequence of V1 holds S₁[p] from FINSEQ_2:sch 2(A4, A2);
hence f . (Sum p) = Sum (f * p) ; :: thesis: verum