deffunc H₁( Nat) -> Element of COMPLEX = Sum (mlt (Line M,$1),F);
consider z being FinSequence of COMPLEX such that
A1: ( len z = len M & ( for i being Nat st i in dom z holds
z . i = H₁(i) ) ) 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 (mlt (Line M,i),F) ) )
dom z = Seg (len M) by A1, FINSEQ_1:def 3;
hence ( len z = len M & ( for i being Nat st i in Seg (len M) holds
z . i = Sum (mlt (Line M,i),F) ) ) by A1; :: thesis: verum