deffunc H₁( set , set ) -> Relation of F₁(),F₂() = F₅($2,$1);
consider F being Function such that
A1: dom F = NAT and
A2: ( F . 0 = F₄() & ( for n being Nat holds F . (n + 1) = H₁(n,F . n) ) ) from NAT_1:sch 11();
reconsider F = F as ManySortedSet of NAT by A1, PARTFUN1:def 2, RELAT_1:def 18;
defpred S₁[ Nat] means F . $1 is Relation of F₁(),F₂();
A3: S₁[ 0 ] by A2;

A4: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[i + 1]
then reconsider R = F . i as Relation of F₁(),F₂() ;
F . (i + 1) = F₅(R,i) by A2;
hence S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
then reconsider R = F . F₃() as Relation of F₁(),F₂() ;
take R ; :: thesis: ex F being ManySortedSet of NAT st
( R = F . F₃() & F . 0 = F₄() & ( for i being Nat
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) )
take F ; :: thesis: ( R = F . F₃() & F . 0 = F₄() & ( for i being Nat
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) )
thus ( R = F . F₃() & F . 0 = F₄() & ( for i being Nat
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) ) by A2; :: thesis: verum