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