deffunc H₁( Nat) -> Element of NAT = In ((width (F . $1)),NAT);
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 by A8, FINSEQ_3:29; :: thesis: for i being Nat st i in dom p holds
p . i = width (F . i)
let i be Nat; :: thesis: ( i in dom p implies p . i = width (F . i) )
assume i in dom p ; :: thesis: p . i = width (F . i)
then p . i = H₁(i) by A9;
hence p . i = width (F . i) ; :: thesis: verum