deffunc H1( object , object ) -> object = [F3(($2 `1),($2 `2),$1),F4(($2 `2),$1)];
consider F being Function such that
A1:
( dom F = NAT & F . 0 = [F1(),F2()] )
and
A2:
for n being Nat holds F . (n + 1) = H1(n,F . n)
from NAT_1:sch 11();
deffunc H2( object ) -> object = (F . $1) `2 ;
deffunc H3( object ) -> object = (F . $1) `1 ;
consider f being ManySortedSet of NAT such that
A3:
for n being object st n in NAT holds
f . n = H3(n)
from PBOOLE:sch 4();
consider h being ManySortedSet of NAT such that
A4:
for n being object st n in NAT holds
h . n = H2(n)
from PBOOLE:sch 4();
take
f
; ex h being ManySortedSet of NAT st
( f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
take
h
; ( f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
( (F . 0) `1 = F1() & (F . 0) `2 = F2() )
by A1;
hence
( f . 0 = F1() & h . 0 = F2() )
by A3, A4; for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) )
let n be Nat; for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) )
let S be non empty ManySortedSign ; for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) )
let x be set ; ( S = f . n & x = h . n implies ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) )
set x = F . n;
A5:
n in NAT
by ORDINAL1:def 12;
then A6:
h . n = (F . n) `2
by A4;
assume
S = f . n
; ( not x = h . n or ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) )
then
S = (F . n) `1
by A3, A5;
then
F . (n + 1) = [F3(S,(h . n),n),F4((h . n),n)]
by A2, A6;
then
( (F . (n + 1)) `1 = F3(S,(h . n),n) & (F . (n + 1)) `2 = F4((h . n),n) )
;
hence
( not x = h . n or ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) )
by A3, A4; verum