reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
deffunc H₁( Nat) -> Element of the carrier of K = M * $1,$1;
consider z being FinSequence of K such that
A1: ( len z = n1 & ( for i being Nat st i in dom z holds
z . i = H₁(i) ) ) from FINSEQ_2:sch 1();
take z ; :: thesis: ( len z = n & ( for i being Nat st i in Seg n holds
z . i = M * i,i ) )
dom z = Seg n1 by A1, FINSEQ_1:def 3;
hence ( len z = n & ( for i being Nat st i in Seg n holds
z . i = M * i,i ) ) by A1; :: thesis: verum