reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
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