deffunc H₁( set , set ) -> object = [[F₄(($2 `11),($2 `2),$1),F₅(($2 `11),($2 `12),($2 `2),$1)],F<sub>6</sub>(($2 `2),$1)];
consider F being Function such that
A1: ( dom F = NAT & F . 0 = [[F₁(),F₂()],F₃()] ) and
A2: for n being Nat holds F . (n + 1) = H₁(n,F . n) from NAT_1:sch 11();
A3: (F . 0) `2 = F<sub>3</sub>() by A1;
deffunc H<sub>2</sub>( object ) -> object = (F . $1) `2 ;
deffunc H₃( object ) -> set = (F . $1) `12 ;
deffunc H<sub>4</sub>( object ) -> set = (F . $1) `11 ;
consider f being ManySortedSet of NAT such that
A4: for n being object st n in NAT holds
f . n = H₄(n) from PBOOLE:sch 4();
consider h being ManySortedSet of NAT such that
A5: for n being object st n in NAT holds
h . n = H₂(n) from PBOOLE:sch 4();
consider g being ManySortedSet of NAT such that
A6: for n being object st n in NAT holds
g . n = H₃(n) from PBOOLE:sch 4();
take f ; :: thesis: ex g, h being ManySortedSet of NAT st
( f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) )
take g ; :: thesis: ex h being ManySortedSet of NAT st
( f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) )
take h ; :: thesis: ( f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) )
( (F . 0) `11 = F<sub>1</sub>() & (F . 0) `12 = F₂() ) by A1, MCART_1:85;
hence ( f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() ) by A4, A6, A5, A3; :: thesis: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) )
let n be Nat; :: thesis: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) )
let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) )
let A be non-empty MSAlgebra over S; :: thesis: for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) )
let x be set ; :: thesis: ( S = f . n & A = g . n & x = h . n implies ( f . (n + 1) = F₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) )
set x = F . n;
A7: n in NAT by ORDINAL1:def 12;
then A8: h . n = (F . n) `2 by A5;
assume that
A9: S = f . n and
A10: A = g . n ; :: thesis: ( not x = h . n or ( f . (n + 1) = F<sub>4</sub>(S,x,n) & g . (n + 1) = F<sub>5</sub>(S,A,x,n) & h . (n + 1) = F<sub>6</sub>(x,n) ) )
A11: A = (F . n) `12 by A6, A7, A10;
S = (F . n) `11 by A4, A7, A9;
then A12: F . (n + 1) = [[F<sub>4</sub>(S,(h . n),n),F<sub>5</sub>(S,A,(h . n),n)],F<sub>6</sub>((h . n),n)] by A2, A11, A8;
then A13: (F . (n + 1)) `2 = F₆((h . n),n) ;
( (F . (n + 1)) `11 = F<sub>4</sub>(S,(h . n),n) & (F . (n + 1)) `12 = F₅(S,A,(h . n),n) ) by A12, MCART_1:85;
hence ( not x = h . n or ( f . (n + 1) = F₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) by A4, A6, A5, A13; :: thesis: verum