deffunc H₁( Nat) -> Element of NAT = len (F . $1);
consider p being FinSequence of NAT such that
A1: len p = len F and
A2: 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 = len (F . i) ) )
thus ( dom p = dom F & ( for i being Nat st i in dom p holds
p . i = len (F . i) ) ) by A1, A2, FINSEQ_3:29; :: thesis: verum