deffunc H₁( Nat) -> Element of D = M * ($1,i);
consider z being FinSequence of D such that
A9: len z = len M and
A10: 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 j being Nat st j in dom M holds
z . j = M * (j,i) ) )
thus len z = len M by A9; :: thesis: for j being Nat st j in dom M holds
z . j = M * (j,i)
let j be Nat; :: thesis: ( j in dom M implies z . j = M * (j,i) )
A11: Seg (len M) = dom M by FINSEQ_1:def 3;
dom z = Seg (len M) by A9, FINSEQ_1:def 3;
hence ( j in dom M implies z . j = M * (j,i) ) by A10, A11; :: thesis: verum