deffunc H₁( object , object ) -> object = [F₃(($2 `1),($2 `2),$1),F₄(($2 `2),$1)];
consider F being Function such that
A1: ( dom F = NAT & F . 0 = [F<sub>1</sub>(),F<sub>2</sub>()] ) and
A2: for n being Nat holds F . (n + 1) = H<sub>1</sub>(n,F . n) from NAT_1:sch 11();
deffunc H<sub>2</sub>( object ) -> object = (F . $1) `2 ;
deffunc H₃( 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 = H<sub>3</sub>(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 = H<sub>2</sub>(n) from PBOOLE:sch 4();
take f ; :: thesis: ex h being ManySortedSet of NAT st
( f . 0 = F<sub>1</sub>() & h . 0 = F<sub>2</sub>() & ( 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) = F<sub>3</sub>(S,x,n) & h . (n + 1) = F<sub>4</sub>(x,n) ) ) )
take h ; :: thesis: ( f . 0 = F<sub>1</sub>() & h . 0 = F<sub>2</sub>() & ( 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) = F<sub>3</sub>(S,x,n) & h . (n + 1) = F<sub>4</sub>(x,n) ) ) )
( (F . 0) `1 = F₁() & (F . 0) `2 = F<sub>2</sub>() ) by A1;
hence ( f . 0 = F<sub>1</sub>() & h . 0 = F<sub>2</sub>() ) by A3, A4; :: thesis: 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) = F<sub>3</sub>(S,x,n) & h . (n + 1) = F<sub>4</sub>(x,n) )
let n be Nat; :: thesis: for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F<sub>3</sub>(S,x,n) & h . (n + 1) = F<sub>4</sub>(x,n) )
let S be non empty ManySortedSign ; :: thesis: for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F<sub>3</sub>(S,x,n) & h . (n + 1) = F<sub>4</sub>(x,n) )
let x be set ; :: thesis: ( S = f . n & x = h . n implies ( f . (n + 1) = F<sub>3</sub>(S,x,n) & h . (n + 1) = F<sub>4</sub>(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 ; :: thesis: ( not x = h . n or ( f . (n + 1) = F₃(S,x,n) & h . (n + 1) = F₄(x,n) ) )
then S = (F . n) `1 by A3, A5;
then F . (n + 1) = [F<sub>3</sub>(S,(h . n),n),F<sub>4</sub>((h . n),n)] by A2, A6;
then ( (F . (n + 1)) `1 = F₃(S,(h . n),n) & (F . (n + 1)) `2 = F₄((h . n),n) ) ;
hence ( not x = h . n or ( f . (n + 1) = F₃(S,x,n) & h . (n + 1) = F₄(x,n) ) ) by A3, A4; :: thesis: verum