deffunc H₁( Nat) -> Element of REAL = Sum (Col (m,$1));
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();
dom e = Seg (width m) by A1, FINSEQ_1:def 3;
hence ex b₁ being FinSequence of REAL st
( len b₁ = width m & ( for j being Nat st j in Seg (width m) holds
b₁ . j = Sum (Col (m,j)) ) ) by A1; :: thesis: verum