let M, N be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for h being Function of the carrier of M, the carrier of N
for s being FinSequence of the carrier of M st h is additive holds
h . (Sum s) = Sum (h * s)
let h be Function of the carrier of M, the carrier of N; :: thesis: for s being FinSequence of the carrier of M st h is additive holds
h . (Sum s) = Sum (h * s)
let s be FinSequence of the carrier of M; :: 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 s being FinSequence of the carrier of M st len s = $1 holds
h . (Sum s) = Sum (h * s);
A2: S₁[ 0 ]

proof

let s be FinSequence of the carrier of M; :: thesis: ( len s = 0 implies h . (Sum s) = Sum (h * s) )
assume A3: len s = 0 ; :: thesis: h . (Sum s) = Sum (h * s)
then Sum s = 0. M by RLVECT_1:75;
then A5: h . (Sum s) = 0. N by A1, Lm39;
s = <*> the carrier of M by A3;
then h * s = <*> the carrier of N ;
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 s be FinSequence of the carrier of M; :: thesis: ( len s = n + 1 implies h . (Sum s) = Sum (h * s) )
set s0 = s | n;
assume A8: len s = n + 1 ; :: thesis: h . (Sum s) = Sum (h * s)
then A9: len (s | n) = n by FINSEQ_1:59, NAT_1:11;
A10: ( 1 <= n + 1 & n + 1 <= len s ) by A8, NAT_1:11;
then A11: s /. (n + 1) = s . (n + 1) by FINSEQ_4:15;
n + 1 in Seg (len s) by A10;
then n + 1 in dom s by FINSEQ_1:def 3;
then reconsider v = s . (n + 1) as Element of M by FINSEQ_2:11;
A12: h * s = h * ((s | n) ^ <*v*>) by A8, A11, FINSEQ_5:21
.= (h * (s | n)) ^ <*(h . v)*> by FINSEQOP:8 ;
h . (Sum s) = h . (Sum ((s | n) ^ <*v*>)) by A8, A11, FINSEQ_5:21
.= h . ((Sum (s | n)) + v) by FVSUM_1:71
.= (h . (Sum (s | n))) + (h . v) by A1
.= (Sum (h * (s | n))) + (h . v) by A7, A9
.= Sum (h * s) by A12, FVSUM_1:71 ;
hence h . (Sum s) = Sum (h * s) ; :: thesis: verum

end;

A13: 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 A13; :: thesis: verum