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