let R be non degenerated Ring; :: thesis: for X being non empty set
for N being LeftMod of R
for h being Homomorphism of id R, Free_LMod (X,R),N
for s being FinSequence of the carrier of (Free_LMod (X,R)) holds h . (Sum s) = Sum (h * s)
let X be non empty set ; :: thesis: for N being LeftMod of R
for h being Homomorphism of id R, Free_LMod (X,R),N
for s being FinSequence of the carrier of (Free_LMod (X,R)) holds h . (Sum s) = Sum (h * s)
let N be LeftMod of R; :: thesis: for h being Homomorphism of id R, Free_LMod (X,R),N
for s being FinSequence of the carrier of (Free_LMod (X,R)) holds h . (Sum s) = Sum (h * s)
let h be Homomorphism of id R, Free_LMod (X,R),N; :: thesis: for s being FinSequence of the carrier of (Free_LMod (X,R)) holds h . (Sum s) = Sum (h * s)
let s be FinSequence of the carrier of (Free_LMod (X,R)); :: thesis: h . (Sum s) = Sum (h * s)
defpred S₁[ Nat] means for s being FinSequence of the carrier of (Free_LMod (X,R)) st len s = $1 holds
h . (Sum s) = Sum (h * s);
A1: S₁[ 0 ]

proof

let s be FinSequence of the carrier of (Free_LMod (X,R)); :: thesis: ( len s = 0 implies h . (Sum s) = Sum (h * s) )
assume A2: len s = 0 ; :: thesis: h . (Sum s) = Sum (h * s)
then s = <*> the carrier of (Free_LMod (X,R)) ;
then A3: Sum s = 0. (Free_LMod (X,R)) by RLVECT_1:43;
h * s = <*> the carrier of N by A2, FINSEQ_2:33;
then Sum (h * s) = 0. N by RLVECT_1:43;
hence h . (Sum s) = Sum (h * s) by A3, Lm38; :: thesis: verum

end;

A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let s be FinSequence of the carrier of (Free_LMod (X,R)); :: thesis: ( len s = k + 1 implies h . (Sum s) = Sum (h * s) )
assume A6: len s = k + 1 ; :: thesis: h . (Sum s) = Sum (h * s)
then consider t being FinSequence of the carrier of (Free_LMod (X,R)), d being Element of (Free_LMod (X,R)) such that
A7: s = t ^ <*d*> by FINSEQ_2:19;
A8: k + 1 = (len t) + 1 by A6, A7, FINSEQ_2:16;
Sum s = (Sum t) + d by A7, FVSUM_1:71;
then A9: h . (Sum s) = (h . (Sum t)) + (h . d) by MOD_4:def 17;
A10: h * (t ^ <*d*>) = (h * t) ^ <*(h . d)*> by Th25;
thus h . (Sum s) = (Sum (h * t)) + (h . d) by A9, A5, A8
.= Sum (h * s) by A7, A10, FVSUM_1:71 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A4);
then S₁[ len s] ;
hence h . (Sum s) = Sum (h * s) ; :: thesis: verum