deffunc H_{1}( 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_{1}(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)

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

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;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