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