let R be domRing; :: thesis: for h being Function of R,R
for s being FinSequence of the carrier of R st h is additive holds
h . (Sum s) = Sum (h * s)
let h be Function of R,R; :: thesis: for s being FinSequence of the carrier of R st h is additive holds
h . (Sum s) = Sum (h * s)
let s be FinSequence of the carrier of R; :: thesis: ( h is additive implies h . (Sum s) = Sum (h * s) )
assume A1: h is additive ; :: thesis: h . (Sum s) = Sum (h * s)
defpred S₁[ Nat] means for h being Function of R,R
for s being FinSequence of R st len s = $1 & h is additive holds
h . (Sum s) = Sum (h * s);
A2: S₁[ 0 ]

proof

let h be Function of R,R; :: thesis: for s being FinSequence of R st len s = 0 & h is additive holds
h . (Sum s) = Sum (h * s)
let s be FinSequence of R; :: thesis: ( len s = 0 & h is additive implies h . (Sum s) = Sum (h * s) )
assume that
A3: len s = 0 and
A4: h is additive ; :: thesis: h . (Sum s) = Sum (h * s)
Sum s = 0. R by A3, RLVECT_1:75;
then A5: h . (Sum s) = 0. R by A4, RING_2:6;
dom h = the carrier of R by FUNCT_2:def 1;
then rng s c= dom h ;
then dom (h * s) = dom s by RELAT_1:27
.= Seg (len s) by FINSEQ_1:def 3 ;
then h * s = <*> the carrier of R by A3;
hence h . (Sum s) = Sum (h * s) by A5, RLVECT_1:43; :: thesis: verum

end;

A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
let h be Function of R,R; :: thesis: for s being FinSequence of R st len s = n + 1 & h is additive holds
h . (Sum s) = Sum (h * s)
let s be FinSequence of R; :: thesis: ( len s = n + 1 & h is additive implies h . (Sum s) = Sum (h * s) )
assume that
A8: len s = n + 1 and
A9: h is additive ; :: thesis: h . (Sum s) = Sum (h * s)
set s0 = s | n;
dom s = Seg (n + 1) by A8, FINSEQ_1:def 3;
then s . (n + 1) in rng s by FUNCT_1:3, FINSEQ_1:4;
then reconsider v = s . (n + 1) as Element of R ;
A10: n = len (s | n) by A8, FINSEQ_1:59, NAT_1:11;
( 1 <= n + 1 & n + 1 <= len s ) by A8, NAT_1:11;
then A11: s /. (len s) = s . (n + 1) by A8, FINSEQ_4:15;
then A12: s = (s | n) ^ <*v*> by A8, FINSEQ_5:21;
A13: h * s = h * ((s | n) ^ <*v*>) by A11, A8, FINSEQ_5:21
.= (h * (s | n)) ^ <*(h . v)*> by FINSEQOP:8 ;
h . (Sum s) = h . ((Sum (s | n)) + (Sum <*v*>)) by A12, RLVECT_1:41
.= h . ((Sum (s | n)) + v) by RLVECT_1:44
.= (h . (Sum (s | n))) + (h . v) by A9
.= (Sum (h * (s | n))) + (h . v) by A7, A9, A10
.= (Sum (h * (s | n))) + (Sum <*(h . v)*>) by RLVECT_1:44
.= Sum (h * s) by A13, RLVECT_1:41 ;
hence h . (Sum s) = Sum (h * s) ; :: thesis: verum

end;

A14: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A6);
len s is Nat ;
hence h . (Sum s) = Sum (h * s) by A1, A14; :: thesis: verum