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