deffunc H₁( Nat) -> Element of the carrier of V1 = Sum (M /. $1);
consider F being FinSequence of V1 such that
A1: ( len F = len M & ( for k being Nat st k in dom F holds
F . k = H₁(k) ) ) from FINSEQ_2:sch 1();
take F ; :: thesis: ( len F = len M & ( for k being Nat st k in dom F holds
F /. k = Sum (M /. k) ) )
thus len F = len M by A1; :: thesis: for k being Nat st k in dom F holds
F /. k = Sum (M /. k)

hereby :: thesis: verum

let k be Nat; :: thesis: ( k in dom F implies F /. k = Sum (M /. k) )
assume A2: k in dom F ; :: thesis: F /. k = Sum (M /. k)
hence F /. k = F . k by PARTFUN1:def 6
.= Sum (M /. k) by A1, A2 ;
:: thesis: verum

end;