deffunc H₁( Nat) -> Element of D = M * (i,$1);
consider f being FinSequence of D such that
A1: len f = width M and
A2: for j being Nat st j in dom f holds
f . j = H₁(j) from FINSEQ_2:sch 1();
take f ; :: thesis: ( len f = width M & ( for j being Nat st j in Seg (width M) holds
f . j = M * (i,j) ) )
thus len f = width M by A1; :: thesis: for j being Nat st j in Seg (width M) holds
f . j = M * (i,j)
let j be Nat; :: thesis: ( j in Seg (width M) implies f . j = M * (i,j) )
dom f = Seg (width M) by A1, FINSEQ_1:def 3;
hence ( j in Seg (width M) implies f . j = M * (i,j) ) by A2; :: thesis: verum