let V1, V2 be Z_Module; :: 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) + (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;
set I0 = 0. INT.Ring;
f . (Sum (<*> the carrier of V1)) = f . (0. V1) by RLVECT_1:43
.= f . ((0. INT.Ring) * (0. V1)) by ZMODUL01:1
.= (0. INT.Ring) * (f . (0. V1)) by A1
.= 0. V2 by ZMODUL01:1
.= 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 FINSEQ_2:sch 2(A4, A2);
 hence f . (Sum p) = Sum (f * p) ; :: thesis: verum