deffunc H₁( Nat) -> Element of REAL = In ((Sum (Col (m,$1))),REAL);
consider e being FinSequence of REAL such that
A1: ( len e = width m & ( for k being Nat st k in dom e holds
e . k = H₁(k) ) ) from FINSEQ_2:sch 1();
take e ; :: thesis: ( len e = width m & ( for j being Nat st j in Seg (width m) holds
e . j = Sum (Col (m,j)) ) )
thus len e = width m by A1; :: thesis: for j being Nat st j in Seg (width m) holds
e . j = Sum (Col (m,j))
let k be Nat; :: thesis: ( k in Seg (width m) implies e . k = Sum (Col (m,k)) )
assume A2: k in Seg (width m) ; :: thesis: e . k = Sum (Col (m,k))
dom e = Seg (width m) by A1, FINSEQ_1:def 3;
then e . k = H₁(k) by A2, A1;
hence e . k = Sum (Col (m,k)) ; :: thesis: verum