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();
A3: dom f = Seg (width M) by A1, FINSEQ_1:def 3;
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 )
thus ( j in Seg (width M) implies f . j = M * i,j ) by A2, A3; :: thesis: verum