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 S1[ 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 S1[p] holds
S1[p ^ <*w*>]
proof
let p be FinSequence of V1; :: thesis: for w being Element of V1 st S1[p] holds
S1[p ^ <*w*>]

let w be Element of V1; :: thesis: ( S1[p] implies S1[p ^ <*w*>] )
assume A3: f . (Sum p) = Sum (f * p) ; :: thesis: S1[p ^ <*w*>]
thus f . (Sum (p ^ <*w*>)) = f . ((Sum p) + ()) by RLVECT_1:41
.= (Sum (f * p)) + (f . ()) by
.= (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
.= 0. V2 by VECTSP_1:14
.= Sum (<*> the carrier of V2) by RLVECT_1:43
.= Sum (f * (<*> the carrier of V1)) ;
then A4: S1[ <*> the carrier of V1] ;
for p being FinSequence of V1 holds S1[p] from hence f . (Sum p) = Sum (f * p) ; :: thesis: verum