deffunc H₁( Nat) -> Element of NAT = width (F . $1);
consider p being FinSequence of NAT such that
A8: len p = len F and
A9: for i being Nat st i in dom p holds
p . i = H₁(i) from FINSEQ_2:sch 1();
take p ; :: thesis: ( dom p = dom F & ( for i being Nat st i in dom p holds
p . i = width (F . i) ) )
thus ( dom p = dom F & ( for i being Nat st i in dom p holds
p . i = width (F . i) ) ) by A8, A9, FINSEQ_3:29; :: thesis: verum