deffunc H1( set , set ) -> Relation of F1(),F2() = F5($2,$1);
consider F being Function such that
A1:
dom F = NAT
and
A2:
( F . 0 = F4() & ( for n being Nat holds F . (n + 1) = H1(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 S1[ Nat] means F . $1 is Relation of F1(),F2();
A3:
S1[ 0 ]
by A2;
A4:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume
S1[
i]
;
S1[i + 1]then reconsider R =
F . i as
Relation of
F1(),
F2() ;
F . (i + 1) = F5(
R,
i)
by A2;
hence
S1[
i + 1]
;
verum end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A3, A4);
then reconsider R = F . F3() as Relation of F1(),F2() ;
take
R
; ex F being ManySortedSet of NAT st
( R = F . F3() & F . 0 = F4() & ( for i being Nat
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) )
take
F
; ( R = F . F3() & F . 0 = F4() & ( for i being Nat
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) )
thus
( R = F . F3() & F . 0 = F4() & ( for i being Nat
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) )
by A2; verum