recdef_2.miz



    begin

    reserve a,b,c,d,e,z for object,

A,B,C,D,E for set;

    definition

      let x be triple object;

      consider x1,x2,x3 be object such that

       A1: x = [x1, x2, x3] by XTUPLE_0:def 5;

      :: original: `1_3

      redefine

      :: RECDEF_2:def1

      func x `1_3 means for y1,y2,y3 be object holds x = [y1, y2, y3] implies it = y1;

      compatibility by A1;

      :: original: `2_3

      redefine

      :: RECDEF_2:def2

      func x `2_3 means for y1,y2,y3 be object holds x = [y1, y2, y3] implies it = y2;

      compatibility by A1;

      :: original: `3_3

      redefine

      :: RECDEF_2:def3

      func x `3_3 means for y1,y2,y3 be object holds x = [y1, y2, y3] implies it = y3;

      compatibility by A1;

    end

    ::$Canceled

    theorem :: RECDEF_2:2

    z in [:A, B, C:] implies (z `1_3 ) in A & (z `2_3 ) in B & (z `3_3 ) in C

    proof

      assume

       A1: z in [:A, B, C:];

      then

       A2: C is non empty by MCART_1: 31;

      

       A3: A is non empty & B is non empty by A1, MCART_1: 31;

      then

      consider a be Element of A, b be Element of B, c be Element of C such that

       A4: z = [a, b, c] by A1, A2, DOMAIN_1: 3;

      

       A5: (z `3_3 ) = c by A4;

      (z `1_3 ) = a & (z `2_3 ) = b by A4;

      hence thesis by A3, A2, A5;

    end;

    theorem :: RECDEF_2:3

    

     Th3: z in [:A, B, C:] implies z = [(z `1_3 ), (z `2_3 ), (z `3_3 )]

    proof

      assume

       A1: z in [:A, B, C:];

      then

       A2: C is non empty by MCART_1: 31;

      A is non empty & B is non empty by A1, MCART_1: 31;

      then ex a be Element of A, b be Element of B, c be Element of C st z = [a, b, c] by A1, A2, DOMAIN_1: 3;

      hence thesis;

    end;

    definition

      let x be quadruple object;

      consider x1,x2,x3,x4 be object such that

       A1: x = [x1, x2, x3, x4] by XTUPLE_0:def 9;

      :: original: `1_4

      redefine

      :: RECDEF_2:def4

      func x `1_4 means for y1,y2,y3,y4 be object holds x = [y1, y2, y3, y4] implies it = y1;

      compatibility by A1;

      :: original: `2_4

      redefine

      :: RECDEF_2:def5

      func x `2_4 means for y1,y2,y3,y4 be object holds x = [y1, y2, y3, y4] implies it = y2;

      compatibility by A1;

      :: original: `3_4

      redefine

      :: RECDEF_2:def6

      func x `3_4 means for y1,y2,y3,y4 be object holds x = [y1, y2, y3, y4] implies it = y3;

      compatibility by A1;

      :: original: `4_4

      redefine

      :: RECDEF_2:def7

      func x `4_4 means for y1,y2,y3,y4 be object holds x = [y1, y2, y3, y4] implies it = y4;

      compatibility by A1;

    end

    ::$Canceled

    theorem :: RECDEF_2:5

    z in [:A, B, C, D:] implies (z `1_4 ) in A & (z `2_4 ) in B & (z `3_4 ) in C & (z `4_4 ) in D

    proof

      assume

       A1: z in [:A, B, C, D:];

      then

       A2: C is non empty & D is non empty by MCART_1: 51;

      

       A3: A is non empty & B is non empty by A1, MCART_1: 51;

      then

      consider a be Element of A, b be Element of B, c be Element of C, d be Element of D such that

       A4: z = [a, b, c, d] by A1, A2, DOMAIN_1: 10;

      

       A5: (z `3_4 ) = c & (z `4_4 ) = d by A4;

      (z `1_4 ) = a & (z `2_4 ) = b by A4;

      hence thesis by A3, A2, A5;

    end;

    theorem :: RECDEF_2:6

    z in [:A, B, C, D:] implies z = [(z `1_4 ), (z `2_4 ), (z `3_4 ), (z `4_4 )]

    proof

      assume

       A1: z in [:A, B, C, D:];

      then

       A2: C is non empty & D is non empty by MCART_1: 51;

      A is non empty & B is non empty by A1, MCART_1: 51;

      then ex a be Element of A, b be Element of B, c be Element of C, d be Element of D st z = [a, b, c, d] by A1, A2, DOMAIN_1: 10;

      hence thesis;

    end;

    definition

      ::$Canceled

    end

    ::$Canceled

    scheme :: RECDEF_2:sch1

    ExFunc3Cond { C() -> set , P,Q,R[ object], F,G,H( object) -> object } :

ex f be Function st ( dom f) = C() & for c be set st c in C() holds (P[c] implies (f . c) = F(c)) & (Q[c] implies (f . c) = G(c)) & (R[c] implies (f . c) = H(c))

      provided

       A1: for c be set st c in C() holds (P[c] implies not Q[c]) & (P[c] implies not R[c]) & (Q[c] implies not R[c])

       and

       A2: for c be set st c in C() holds P[c] or Q[c] or R[c];

      consider D1 be set such that

       A3: for x be object holds x in D1 iff x in C() & P[x] from XBOOLE_0:sch 1;

      consider D3 be set such that

       A4: for x be object holds x in D3 iff x in C() & R[x] from XBOOLE_0:sch 1;

      consider f1 be Function such that

       A5: ( dom f1) = D1 and

       A6: for x be object st x in D1 holds (f1 . x) = F(x) from FUNCT_1:sch 3;

      consider D2 be set such that

       A7: for x be object holds x in D2 iff x in C() & Q[x] from XBOOLE_0:sch 1;

      consider f3 be Function such that

       A8: ( dom f3) = D3 and

       A9: for x be object st x in D3 holds (f3 . x) = H(x) from FUNCT_1:sch 3;

      consider f2 be Function such that

       A10: ( dom f2) = D2 and

       A11: for x be object st x in D2 holds (f2 . x) = G(x) from FUNCT_1:sch 3;

      set f = ((f1 +* f2) +* f3);

      take f;

      

       A12: ( dom f) = (( dom (f1 +* f2)) \/ ( dom f3)) by FUNCT_4:def 1

      .= ((( dom f1) \/ ( dom f2)) \/ ( dom f3)) by FUNCT_4:def 1;

      thus ( dom f) = C()

      proof

        

         A13: D3 c= C() by A4;

        

         A14: D2 c= C() by A7;

        D1 c= C() by A3;

        then (D1 \/ D2) c= C() by A14, XBOOLE_1: 8;

        hence ( dom f) c= C() by A5, A10, A8, A12, A13, XBOOLE_1: 8;

        let x be object;

        assume

         A15: x in C();

        then P[x] or Q[x] or R[x] by A2;

        then x in D1 or x in D2 or x in D3 by A3, A7, A4, A15;

        then x in (D1 \/ D2) or x in D3 by XBOOLE_0:def 3;

        hence thesis by A5, A10, A8, A12, XBOOLE_0:def 3;

      end;

      let c be set such that

       A16: c in C();

      hereby

        assume

         A17: P[c];

         not Q[c] by A1, A16, A17;

        then

         A18: not c in D2 by A7;

         not R[c] by A1, A16, A17;

        then not c in D3 by A4;

        

        hence (f . c) = ((f1 +* f2) . c) by A8, FUNCT_4: 11

        .= (f1 . c) by A10, A18, FUNCT_4: 11

        .= F(c) by A6, A17, A3, A16;

      end;

      hereby

        assume

         A19: Q[c];

         not R[c] by A1, A16, A19;

        then not c in D3 by A4;

        

        hence (f . c) = ((f1 +* f2) . c) by A8, FUNCT_4: 11

        .= (f2 . c) by A10, A19, A7, A16, FUNCT_4: 13

        .= G(c) by A11, A19, A7, A16;

      end;

      assume

       A20: R[c];

      

      hence (f . c) = (f3 . c) by A8, A4, A16, FUNCT_4: 13

      .= H(c) by A9, A20, A4, A16;

    end;

    scheme :: RECDEF_2:sch2

    ExFunc4Cond { C() -> set , P,Q,R,S[ object], F,G,H,I( object) -> object } :

ex f be Function st ( dom f) = C() & for c be set st c in C() holds (P[c] implies (f . c) = F(c)) & (Q[c] implies (f . c) = G(c)) & (R[c] implies (f . c) = H(c)) & (S[c] implies (f . c) = I(c))

      provided

       A1: for c be set st c in C() holds (P[c] implies not Q[c]) & (P[c] implies not R[c]) & (P[c] implies not S[c]) & (Q[c] implies not R[c]) & (Q[c] implies not S[c]) & (R[c] implies not S[c])

       and

       A2: for c be set st c in C() holds P[c] or Q[c] or R[c] or S[c];

      consider D1 be set such that

       A3: for x be object holds x in D1 iff x in C() & P[x] from XBOOLE_0:sch 1;

      consider D4 be set such that

       A4: for x be object holds x in D4 iff x in C() & S[x] from XBOOLE_0:sch 1;

      consider f1 be Function such that

       A5: ( dom f1) = D1 and

       A6: for x be object st x in D1 holds (f1 . x) = F(x) from FUNCT_1:sch 3;

      consider D2 be set such that

       A7: for x be object holds x in D2 iff x in C() & Q[x] from XBOOLE_0:sch 1;

      consider f2 be Function such that

       A8: ( dom f2) = D2 and

       A9: for x be object st x in D2 holds (f2 . x) = G(x) from FUNCT_1:sch 3;

      consider D3 be set such that

       A10: for x be object holds x in D3 iff x in C() & R[x] from XBOOLE_0:sch 1;

      consider f4 be Function such that

       A11: ( dom f4) = D4 and

       A12: for x be object st x in D4 holds (f4 . x) = I(x) from FUNCT_1:sch 3;

      consider f3 be Function such that

       A13: ( dom f3) = D3 and

       A14: for x be object st x in D3 holds (f3 . x) = H(x) from FUNCT_1:sch 3;

      set f = (((f1 +* f2) +* f3) +* f4);

      take f;

      

       A15: ( dom f) = (( dom ((f1 +* f2) +* f3)) \/ ( dom f4)) by FUNCT_4:def 1

      .= ((( dom (f1 +* f2)) \/ ( dom f3)) \/ ( dom f4)) by FUNCT_4:def 1

      .= (((( dom f1) \/ ( dom f2)) \/ ( dom f3)) \/ ( dom f4)) by FUNCT_4:def 1;

      thus ( dom f) = C()

      proof

        

         A16: D4 c= C() by A4;

        

         A17: D3 c= C() by A10;

        

         A18: D2 c= C() by A7;

        D1 c= C() by A3;

        then (D1 \/ D2) c= C() by A18, XBOOLE_1: 8;

        then ((D1 \/ D2) \/ D3) c= C() by A17, XBOOLE_1: 8;

        hence ( dom f) c= C() by A5, A8, A13, A11, A15, A16, XBOOLE_1: 8;

        let x be object;

        assume

         A19: x in C();

        then P[x] or Q[x] or R[x] or S[x] by A2;

        then x in D1 or x in D2 or x in D3 or x in D4 by A3, A7, A10, A4, A19;

        then x in (D1 \/ D2) or x in D3 or x in D4 by XBOOLE_0:def 3;

        then x in ((D1 \/ D2) \/ D3) or x in D4 by XBOOLE_0:def 3;

        hence thesis by A5, A8, A13, A11, A15, XBOOLE_0:def 3;

      end;

      let c be set such that

       A20: c in C();

      hereby

        assume

         A21: P[c];

         not R[c] by A1, A20, A21;

        then

         A22: not c in D3 by A10;

         not Q[c] by A1, A20, A21;

        then

         A23: not c in D2 by A7;

         not S[c] by A1, A20, A21;

        then not c in D4 by A4;

        

        hence (f . c) = (((f1 +* f2) +* f3) . c) by A11, FUNCT_4: 11

        .= ((f1 +* f2) . c) by A13, A22, FUNCT_4: 11

        .= (f1 . c) by A8, A23, FUNCT_4: 11

        .= F(c) by A6, A21, A3, A20;

      end;

      hereby

        assume

         A24: Q[c];

         not R[c] by A1, A20, A24;

        then

         A25: not c in D3 by A10;

         not S[c] by A1, A20, A24;

        then not c in D4 by A4;

        

        hence (f . c) = (((f1 +* f2) +* f3) . c) by A11, FUNCT_4: 11

        .= ((f1 +* f2) . c) by A13, A25, FUNCT_4: 11

        .= (f2 . c) by A8, A24, A7, A20, FUNCT_4: 13

        .= G(c) by A9, A24, A7, A20;

      end;

      hereby

        assume

         A26: R[c];

         not S[c] by A1, A20, A26;

        then not c in D4 by A4;

        

        hence (f . c) = (((f1 +* f2) +* f3) . c) by A11, FUNCT_4: 11

        .= (f3 . c) by A13, A26, A10, A20, FUNCT_4: 13

        .= H(c) by A14, A26, A10, A20;

      end;

      assume

       A27: S[c];

      

      hence (f . c) = (f4 . c) by A11, A4, A20, FUNCT_4: 13

      .= I(c) by A12, A27, A4, A20;

    end;

    scheme :: RECDEF_2:sch3

    DoubleChoiceRec { A,B() -> non empty set , A0() -> Element of A() , B0() -> Element of B() , P[ object, object, object, object, object] } :

ex f be sequence of A(), g be sequence of B() st (f . 0 ) = A0() & (g . 0 ) = B0() & for n be Nat holds P[n, (f . n), (g . n), (f . (n + 1)), (g . (n + 1))]

      provided

       A1: for n be Nat, x be Element of A(), y be Element of B() holds ex x1 be Element of A(), y1 be Element of B() st P[n, x, y, x1, y1];

      defpred P1[ set, set, set] means P[$1, ($2 `1 ), ($2 `2 ), ($3 `1 ), ($3 `2 )];

      

       A2: for n be Nat, x be Element of [:A(), B():] holds ex y be Element of [:A(), B():] st P1[n, x, y]

      proof

        let n be Nat, x be Element of [:A(), B():];

        consider ai be Element of A(), bi be Element of B() such that

         A3: P[n, (x `1 ), (x `2 ), ai, bi] by A1;

        take [ai, bi];

        thus thesis by A3;

      end;

      consider f be sequence of [:A(), B():] such that

       A4: (f . 0 ) = [A0(), B0()] and

       A5: for e be Nat holds P1[e, (f . e), (f . (e + 1))] from RECDEF_1:sch 2( A2);

      take ( pr1 f), ( pr2 f);

      ( [A0(), B0()] `1 ) = A0() & ( [A0(), B0()] `2 ) = B0();

      hence (( pr1 f) . 0 ) = A0() & (( pr2 f) . 0 ) = B0() by A4, FUNCT_2:def 5, FUNCT_2:def 6;

      let i be Nat;

      

       A6: ((f . (i + 1)) `1 ) = (( pr1 f) . (i + 1)) & ((f . (i + 1)) `2 ) = (( pr2 f) . (i + 1)) by FUNCT_2:def 5, FUNCT_2:def 6;

      i in NAT by ORDINAL1:def 12;

      then ((f . i) `1 ) = (( pr1 f) . i) & ((f . i) `2 ) = (( pr2 f) . i) by FUNCT_2:def 5, FUNCT_2:def 6;

      hence thesis by A5, A6;

    end;

    scheme :: RECDEF_2:sch4

    LambdaRec2Ex { A,B() -> set , F( object, object, object) -> object } :

ex f be Function st ( dom f) = NAT & (f . 0 ) = A() & (f . 1) = B() & for n be Nat holds (f . (n + 2)) = F(n,.,.);

      defpred C[ set] means $1 = 0 ;

      deffunc G( Nat, set) = [($2 `2_3 ), ($2 `3_3 ), F(+,`2_3,`3_3)];

      set r03 = F(0,A,B);

      set r13 = F(,B,r03);

      deffunc H( Nat, set) = G(+,$2);

      consider h be Function such that ( dom h) = NAT and

       A1: (h . 0 ) = [B(), r03, r13] and

       A2: for n be Nat holds (h . (n + 1)) = H(n,.) from NAT_1:sch 11;

      deffunc Y( Nat) = (h . ($1 -' 1));

      deffunc X( set) = [A(), B(), r03];

      consider g be Function such that ( dom g) = NAT and

       A3: for x be Element of NAT holds ( C[x] implies (g . x) = X(x)) & ( not C[x] implies (g . x) = Y(x)) from PARTFUN1:sch 4;

      deffunc M( object) = ((g . $1) `1_3 );

      consider f be Function such that

       A4: ( dom f) = NAT and

       A5: for x be object st x in NAT holds (f . x) = M(x) from FUNCT_1:sch 3;

      defpred P[ Nat] means (f . ($1 + 2)) = ((g . ($1 + 1)) `2_3 ) & ((g . ($1 + 1)) `1_3 ) = ((g . $1) `2_3 ) & ((g . ($1 + 2)) `1_3 ) = ((g . $1) `3_3 ) & ((g . ($1 + 2)) `1_3 ) = ((g . ($1 + 1)) `2_3 ) & ((g . ($1 + 2)) `2_3 ) = ((g . ($1 + 1)) `3_3 ) & (f . ($1 + 2)) = F($1,.,.);

      

       A6: (g . 0 ) = [A(), B(), r03] by A3;

      

       A7: for n be Nat holds (g . (n + 2)) = G(+,.)

      proof

        let n be Nat;

        

         A8: ((n + 2) - 1) = (n + (2 - 1)) & 0 <= (n + 1);

        

         A9: (g . (n + 1)) = Y(+) by A3

        .= (h . n) by NAT_D: 34;

        

        thus (g . (n + 2)) = Y(+) by A3

        .= (h . (n + 1)) by A8, XREAL_0:def 2

        .= G(+,.) by A2, A9;

      end;

      

      then

       A10: ((g . ( 0 + 2)) `2_3 ) = ( G(+,.) `2_3 )

      .= ((g . ( 0 + 1)) `3_3 );

      take f;

      thus ( dom f) = NAT by A4;

      

      thus

       A11: (f . 0 ) = ((g . 0 ) `1_3 ) by A5

      .= A() by A6;

      

       A12: (g . 1) = Y() by A3

      .= [B(), r03, r13] by A1, XREAL_1: 232;

      

      then

       A13: ((g . ( 0 + 1)) `1_3 ) = B()

      .= ((g . 0 ) `2_3 ) by A6;

      

       A14: for x be Nat st P[x] holds P[(x + 1)]

      proof

        let x be Nat;

        assume

         A15: P[x];

        then

         A16: (f . (x + 1)) = ((g . x) `2_3 ) by A5;

        

        thus

         A17: (f . ((x + 1) + 2)) = ((g . ((x + 1) + 2)) `1_3 ) by A5

        .= ( G(+,.) `1_3 ) by A7

        .= ((g . ((x + 1) + 1)) `2_3 );

        thus ((g . ((x + 1) + 1)) `1_3 ) = ((g . (x + 1)) `2_3 ) by A15;

        

        thus ((g . ((x + 1) + 2)) `1_3 ) = ( G(+,.) `1_3 ) by A7

        .= ((g . (x + 1)) `3_3 ) by A15;

        hence ((g . ((x + 1) + 2)) `1_3 ) = ((g . ((x + 1) + 1)) `2_3 ) by A15;

        

        thus ((g . ((x + 1) + 2)) `2_3 ) = ( G(+,.) `2_3 ) by A7

        .= ((g . ((x + 1) + 1)) `3_3 );

        per cases ;

          suppose

           A18: x = 0 ;

          

          hence (f . ((x + 1) + 2)) = ((g . (1 + 2)) `1_3 ) by A5

          .= ( G(+,.) `1_3 ) by A7

          .= ((g . ( 0 + 1)) `3_3 ) by A15, A18

          .= r13 by A12

          .= F(+,B,`3_3) by A6

          .= F(+,.,.) by A6, A15, A16, A18;

        end;

          suppose x <> 0 ;

          then 0 < x;

          then

           A19: ( 0 + 1) <= x by NAT_1: 13;

          then

           A20: ((x -' 1) + 1) = x by XREAL_1: 235;

          (1 - 1) <= (x - 1) by A19, XREAL_1: 13;

          then

           A21: (x - 1) = (x -' 1) by XREAL_0:def 2;

          (x + 1) = ((x - 1) + 2);

          

          hence (f . ((x + 1) + 2)) = ( G(+,.) `3_3 ) by A7, A15, A17, A21

          .= F(+,.,.) by A15, A16, A20;

        end;

      end;

      

       A22: (f . ( 0 + 2)) = ((g . ( 0 + 2)) `1_3 ) by A5

      .= ( G(+,.) `1_3 ) by A7

      .= ((g . ( 0 + 1)) `2_3 );

      

      thus

       A23: (f . 1) = ((g . 1) `1_3 ) by A5

      .= B() by A12;

      

       A24: ((g . ( 0 + 2)) `1_3 ) = ( G(+,.) `1_3 ) by A7

      .= ((g . 1) `2_3 )

      .= r03 by A12

      .= ((g . 0 ) `3_3 ) by A6;

      

      then ((g . ( 0 + 2)) `1_3 ) = r03 by A6

      .= ((g . ( 0 + 1)) `2_3 ) by A12;

      then

       A25: P[ 0 ] by A12, A11, A23, A22, A13, A24, A10;

      for x be Nat holds P[x] from NAT_1:sch 2( A25, A14);

      hence thesis;

    end;

    scheme :: RECDEF_2:sch5

    LambdaRec2ExD { X() -> non empty set , A,B() -> Element of X() , F( object, object, object) -> Element of X() } :

ex f be sequence of X() st (f . 0 ) = A() & (f . 1) = B() & for n be Nat holds (f . (n + 2)) = F(n,.,.);

      consider f be Function such that

       A1: ( dom f) = NAT and

       A2: (f . 0 ) = A() & (f . 1) = B() and

       A3: for n be Nat holds (f . (n + 2)) = F(n,.,.) from LambdaRec2Ex;

      ( rng f) c= X()

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider n be object such that

         A4: n in ( dom f) and

         A5: (f . n) = y by FUNCT_1:def 3;

        reconsider n as Nat by A1, A4;

        per cases ;

          suppose n <= 1;

          then n = 0 or n = 1 by NAT_1: 25;

          hence thesis by A2, A5;

        end;

          suppose n > 1;

          then (1 + 1) <= n by NAT_1: 13;

          then (n - 2) in NAT by INT_1: 5;

          then (f . ((n - 2) + 2)) = F(-,.,.) by A3;

          hence thesis by A5;

        end;

      end;

      then f is sequence of X() by A1, FUNCT_2:def 1, RELSET_1: 4;

      hence thesis by A2, A3;

    end;

    scheme :: RECDEF_2:sch6

    LambdaRec2Un { A,B() -> object , F,G() -> Function , F( object, object, object) -> object } :

F() = G()

      provided

       A1: ( dom F()) = NAT

       and

       A2: (F() . 0 ) = A() & (F() . 1) = B()

       and

       A3: for n be Nat holds (F() . (n + 2)) = F(n,.,.)

       and

       A4: ( dom G()) = NAT

       and

       A5: (G() . 0 ) = A() & (G() . 1) = B()

       and

       A6: for n be Nat holds (G() . (n + 2)) = F(n,.,.);

      defpred Q[ Nat] means (F() . $1) <> (G() . $1);

      assume F() <> G();

      then ex x be object st x in NAT & (F() . x) <> (G() . x) by A1, A4, FUNCT_1: 2;

      then

       A7: ex k be Nat st Q[k];

      consider m be Nat such that

       A8: Q[m] and

       A9: for n be Nat st Q[n] holds m <= n from NAT_1:sch 5( A7);

      now

        set k = (m -' 2);

        

         A10: (F() . (k + 2)) = F(k,.,.) & (G() . (k + 2)) = F(k,.,.) by A3, A6;

        assume m <> 0 & m <> 1;

        then 1 < m by NAT_1: 25;

        then (1 + 1) <= m by NAT_1: 13;

        then

         A11: m = (k + 2) by XREAL_1: 235;

        then

         A12: (F() . (k + 1)) = (G() . (k + 1)) by A9, XREAL_1: 6;

        (k + 0 ) < m by A11, XREAL_1: 6;

        hence contradiction by A8, A9, A11, A12, A10;

      end;

      hence contradiction by A2, A5, A8;

    end;

    scheme :: RECDEF_2:sch7

    LambdaRec2UnD { X() -> non empty set , A,B() -> Element of X() , F,G() -> sequence of X() , F( object, object, object) -> Element of X() } :

F() = G()

      provided

       A1: (F() . 0 ) = A() & (F() . 1) = B()

       and

       A2: for n be Nat holds (F() . (n + 2)) = F(n,.,.)

       and

       A3: (G() . 0 ) = A() & (G() . 1) = B()

       and

       A4: for n be Nat holds (G() . (n + 2)) = F(n,.,.);

      

       A5: ( dom G()) = NAT by FUNCT_2:def 1;

      

       A6: ( dom F()) = NAT by FUNCT_2:def 1;

      thus F() = G() from LambdaRec2Un( A6, A1, A2, A5, A3, A4);

    end;

    scheme :: RECDEF_2:sch8

    LambdaRec3Ex { A,B,C() -> set , F( object, object, object, object) -> object } :

ex f be Function st ( dom f) = NAT & (f . 0 ) = A() & (f . 1) = B() & (f . 2) = C() & for n be Nat holds (f . (n + 3)) = F(n,.,.,.);

      defpred C3[ object] means ( In ($1, NAT )) > 1;

      defpred C2[ object] means $1 = 1;

      defpred C1[ object] means $1 = 0 ;

      deffunc G( Nat, set) = [($2 `2_4 ), ($2 `3_4 ), ($2 `4_4 ), F(+,`2_4,`3_4,`4_4)];

      set r04 = F(0,A,B,C);

      set r14 = F(,B,C,r04);

      set r24 = F(,C,r04,r14);

      deffunc H( Nat, set) = G(+,$2);

      consider h be Function such that ( dom h) = NAT and

       A1: (h . 0 ) = [C(), r04, r14, r24] and

       A2: for n be Nat holds (h . (n + 1)) = H(n,.) from NAT_1:sch 11;

      deffunc X3( object) = (h . (( In ($1, NAT )) -' 2));

      deffunc X2( object) = [B(), C(), r04, r14];

      deffunc X1( object) = [A(), B(), C(), r04];

      

       A3: for c be set st c in NAT holds C1[c] or C2[c] or C3[c]

      proof

        let c be set;

        assume c in NAT ;

        then ( In (c, NAT )) = c by SUBSET_1:def 8;

        hence thesis by NAT_1: 25;

      end;

      

       A4: for c be set st c in NAT holds ( C1[c] implies not C2[c]) & ( C1[c] implies not C3[c]) & ( C2[c] implies not C3[c]);

      consider g be Function such that ( dom g) = NAT and

       A5: for x be set st x in NAT holds ( C1[x] implies (g . x) = X1(x)) & ( C2[x] implies (g . x) = X2(x)) & ( C3[x] implies (g . x) = X3(x)) from ExFunc3Cond( A4, A3);

      

       A6: (g . 2) = X3() by A5

      .= [C(), r04, r14, r24] by A1, XREAL_1: 232;

      

       A7: for n be Nat holds (g . (n + 3)) = G(+,.)

      proof

        let n be Nat;

        ( 0 + 1) < (n + 2) by XREAL_1: 8;

        

        then

         A8: (g . (n + 2)) = X3(+) by A5

        .= (h . n) by NAT_D: 34;

        

         A9: ((n + 3) - 2) = (n + (3 - 2)) & 0 <= (n + 1);

        ( 0 + 1) < (n + 3) by XREAL_1: 8;

        

        hence (g . (n + 3)) = X3(+) by A5

        .= (h . (n + 1)) by A9, XREAL_0:def 2

        .= G(+,.) by A2, A8;

      end;

      

       A10: (g . 1) = [B(), C(), r04, r14] by A5;

      

      then

       A11: ((g . ( 0 + 1)) `3_4 ) = r04

      .= ((g . ( 0 + 2)) `2_4 ) by A6;

      

       A12: (g . 0 ) = [A(), B(), C(), r04] by A5;

      

      then

       A13: ((g . 0 ) `3_4 ) = C()

      .= ((g . ( 0 + 1)) `2_4 ) by A10;

      

       A14: ((g . ( 0 + 1)) `4_4 ) = r14 by A10

      .= ((g . ( 0 + 2)) `3_4 ) by A6;

      

       A15: ((g . 0 ) `4_4 ) = r04 by A12

      .= ((g . ( 0 + 1)) `3_4 ) by A10;

      

       A16: ((g . ( 0 + 1)) `1_4 ) = B() by A10

      .= ((g . 0 ) `2_4 ) by A12;

      deffunc M( Nat) = ((g . $1) `1_4 );

      consider f be Function such that

       A17: ( dom f) = NAT and

       A18: for x be Element of NAT holds (f . x) = M(x) from FUNCT_1:sch 4;

      

       A19: (f . ( 0 + 3)) = ((g . ( 0 + 3)) `1_4 ) by A18

      .= ( G(+,.) `1_4 ) by A7

      .= ((g . ( 0 + 2)) `2_4 );

      take f;

      thus ( dom f) = NAT by A17;

      defpred P[ Nat] means (f . ($1 + 3)) = ((g . ($1 + 2)) `2_4 ) & ((g . $1) `2_4 ) = ((g . ($1 + 1)) `1_4 ) & ((g . $1) `3_4 ) = ((g . ($1 + 1)) `2_4 ) & ((g . $1) `4_4 ) = ((g . ($1 + 1)) `3_4 ) & ((g . ($1 + 1)) `2_4 ) = ((g . ($1 + 2)) `1_4 ) & ((g . ($1 + 1)) `3_4 ) = ((g . ($1 + 2)) `2_4 ) & ((g . ($1 + 1)) `4_4 ) = ((g . ($1 + 2)) `3_4 ) & ((g . ($1 + 2)) `2_4 ) = ((g . ($1 + 3)) `1_4 ) & (f . ($1 + 3)) = F($1,.,.,.);

      

       A20: ((g . ( 0 + 2)) `2_4 ) = ( G(+,.) `1_4 )

      .= ((g . ( 0 + 3)) `1_4 ) by A7;

      

      thus

       A21: (f . 0 ) = ((g . 0 ) `1_4 ) by A18

      .= A() by A12;

      

      thus

       A22: (f . 1) = ((g . 1) `1_4 ) by A18

      .= B() by A10;

      

      thus

       A23: (f . 2) = ((g . 2) `1_4 ) by A18

      .= C() by A6;

      

       A24: for x be Nat st P[x] holds P[(x + 1)]

      proof

        let x be Nat;

        

         A25: ((x + 1) + 2) = (x + (1 + 2));

        assume

         A26: P[x];

        then

         A27: (f . ((x + 1) + 1)) = ((g . x) `3_4 ) by A18;

        

        thus

         A28: (f . ((x + 1) + 3)) = ((g . ((x + 1) + 3)) `1_4 ) by A18

        .= ( G(+,.) `1_4 ) by A7

        .= ((g . ((x + 1) + 2)) `2_4 );

        thus ((g . ((x + 1) + 1)) `1_4 ) = ((g . (x + 1)) `2_4 ) by A26;

        thus ((g . (x + 1)) `3_4 ) = ((g . ((x + 1) + 1)) `2_4 ) by A26;

        thus ((g . (x + 1)) `4_4 ) = ((g . ((x + 1) + 1)) `3_4 ) by A26;

        

        thus ((g . ((x + 1) + 1)) `2_4 ) = ( G(+,.) `1_4 )

        .= ((g . ((x + 1) + 2)) `1_4 ) by A7, A25;

        

        thus ((g . ((x + 1) + 1)) `3_4 ) = ( G(+,.) `2_4 )

        .= ((g . ((x + 1) + 2)) `2_4 ) by A7, A25;

        

        thus ((g . ((x + 1) + 1)) `4_4 ) = ( G(+,.) `3_4 )

        .= ((g . ((x + 1) + 2)) `3_4 ) by A7, A25;

        

        thus ((g . ((x + 1) + 2)) `2_4 ) = ( G(+,.) `1_4 )

        .= ((g . ((x + 1) + 3)) `1_4 ) by A7;

        per cases ;

          suppose x <= 1 & x <> 1;

          then

           A29: x = 0 by NAT_1: 25;

          

          hence (f . ((x + 1) + 3)) = ((g . (1 + 3)) `1_4 ) by A18

          .= ( G(+,.) `1_4 ) by A7

          .= ((g . ( 0 + 3)) `2_4 )

          .= ( G(+,.) `2_4 ) by A7

          .= ((g . ( 0 + 2)) `3_4 )

          .= r14 by A6

          .= F(+,.,.,.) by A12, A22, A23, A26, A29;

        end;

          suppose

           A30: x = 1;

          then

           A31: (f . ((x + 1) + 1)) = r04 & (f . ((x + 1) + 2)) = r14 by A10, A26, A27;

          

          thus (f . ((x + 1) + 3)) = ((g . ((1 + 1) + 3)) `1_4 ) by A18, A30

          .= ( G(+,.) `1_4 ) by A7

          .= ((g . (1 + 3)) `2_4 )

          .= ( G(+,.) `2_4 ) by A7

          .= ((g . ( 0 + 3)) `3_4 )

          .= ( G(+,.) `3_4 ) by A7

          .= ((g . ( 0 + 2)) `4_4 )

          .= F(+,.,.,.) by A6, A23, A30, A31;

        end;

          suppose

           A32: 1 < x;

          then (1 - 1) <= (x - 1) by XREAL_1: 13;

          then

           A33: (x - 1) = (x -' 1) by XREAL_0:def 2;

          

           A34: (1 + 1) <= x by A32, NAT_1: 13;

          then

           A35: ((x -' 2) + 2) = x by XREAL_1: 235;

          (2 - 2) <= (x - 2) by A34, XREAL_1: 13;

          then

           A36: (x - 2) = (x -' 2) by XREAL_0:def 2;

          

           A37: (x + 1) = ((x - 1) + 2);

          

          thus (f . ((x + 1) + 3)) = ((g . (x + (1 + 2))) `2_4 ) by A28

          .= ( G(+,.) `2_4 ) by A7

          .= ((g . ((x -' 1) + 3)) `3_4 ) by A33

          .= ( G(+,.) `3_4 ) by A7, A33, A37

          .= ((g . ((x -' 2) + 3)) `4_4 ) by A36

          .= ( G(+,.) `4_4 ) by A7

          .= F(+,`2_4,`3_4,`4_4) by A35

          .= F(+,.,.,.) by A18, A26, A27;

        end;

      end;

      ((g . ( 0 + 1)) `2_4 ) = C() by A10

      .= ((g . ( 0 + 2)) `1_4 ) by A6;

      then

       A38: P[ 0 ] by A6, A21, A22, A23, A19, A16, A13, A15, A11, A14, A20;

      for x be Nat holds P[x] from NAT_1:sch 2( A38, A24);

      hence thesis;

    end;

    scheme :: RECDEF_2:sch9

    LambdaRec3ExD { X() -> non empty set , A,B,C() -> Element of X() , F( object, object, object, object) -> Element of X() } :

ex f be sequence of X() st (f . 0 ) = A() & (f . 1) = B() & (f . 2) = C() & for n be Nat holds (f . (n + 3)) = F(n,.,.,.);

      consider f be Function such that

       A1: ( dom f) = NAT and

       A2: (f . 0 ) = A() & (f . 1) = B() & (f . 2) = C() and

       A3: for n be Nat holds (f . (n + 3)) = F(n,.,.,.) from LambdaRec3Ex;

      ( rng f) c= X()

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider n be object such that

         A4: n in ( dom f) and

         A5: (f . n) = y by FUNCT_1:def 3;

        reconsider n as Nat by A1, A4;

        per cases ;

          suppose n <= 2;

          then n = 0 or ... or n = 2;

          hence thesis by A2, A5;

        end;

          suppose n > 2;

          then (2 + 1) <= n by NAT_1: 13;

          then (n - 3) in NAT by INT_1: 5;

          then (f . ((n - 3) + 3)) = F(-,.,.,.) by A3;

          hence thesis by A5;

        end;

      end;

      then f is sequence of X() by A1, FUNCT_2:def 1, RELSET_1: 4;

      hence thesis by A2, A3;

    end;

    scheme :: RECDEF_2:sch10

    LambdaRec3Un { A,B,C() -> object , F,G() -> Function , F( object, object, object, object) -> object } :

F() = G()

      provided

       A1: ( dom F()) = NAT

       and

       A2: (F() . 0 ) = A() & (F() . 1) = B() & (F() . 2) = C()

       and

       A3: for n be Nat holds (F() . (n + 3)) = F(n,.,.,.)

       and

       A4: ( dom G()) = NAT

       and

       A5: (G() . 0 ) = A() & (G() . 1) = B() & (G() . 2) = C()

       and

       A6: for n be Nat holds (G() . (n + 3)) = F(n,.,.,.);

      defpred Q[ Nat] means (F() . $1) <> (G() . $1);

      assume F() <> G();

      then ex x be object st x in NAT & (F() . x) <> (G() . x) by A1, A4, FUNCT_1: 2;

      then

       A7: ex k be Nat st Q[k];

      consider m be Nat such that

       A8: Q[m] and

       A9: for n be Nat st Q[n] holds m <= n from NAT_1:sch 5( A7);

      now

        set k = (m -' 3);

        

         A10: (F() . (k + 3)) = F(k,.,.,.) & (G() . (k + 3)) = F(k,.,.,.) by A3, A6;

        assume m <> 0 & ... & m <> 2;

        then 2 < m;

        then (2 + 1) <= m by NAT_1: 13;

        then

         A11: m = (k + 3) by XREAL_1: 235;

        then

         A12: (F() . (k + 1)) = (G() . (k + 1)) by A9, XREAL_1: 6;

        

         A13: (F() . (k + 2)) = (G() . (k + 2)) by A9, A11, XREAL_1: 6;

        (k + 0 ) < m by A11, XREAL_1: 6;

        hence contradiction by A8, A9, A11, A12, A13, A10;

      end;

      hence contradiction by A2, A5, A8;

    end;

    scheme :: RECDEF_2:sch11

    LambdaRec3UnD { X() -> non empty set , A,B,C() -> Element of X() , F,G() -> sequence of X() , F( object, object, object, object) -> Element of X() } :

F() = G()

      provided

       A1: (F() . 0 ) = A() & (F() . 1) = B() & (F() . 2) = C()

       and

       A2: for n be Nat holds (F() . (n + 3)) = F(n,.,.,.)

       and

       A3: (G() . 0 ) = A() & (G() . 1) = B() & (G() . 2) = C()

       and

       A4: for n be Nat holds (G() . (n + 3)) = F(n,.,.,.);

      

       A5: ( dom G()) = NAT by FUNCT_2:def 1;

      

       A6: ( dom F()) = NAT by FUNCT_2:def 1;

      thus F() = G() from LambdaRec3Un( A6, A1, A2, A5, A3, A4);

    end;

    scheme :: RECDEF_2:sch12

    LambdaRec4Un { A,B,C,D() -> object , F,G() -> Function , F( object, object, object, object, object) -> object } :

F() = G()

      provided

       A1: ( dom F()) = NAT

       and

       A2: (F() . 0 ) = A() & (F() . 1) = B() & (F() . 2) = C() & (F() . 3) = D()

       and

       A3: for n be Nat holds (F() . (n + 4)) = F(n,.,.,.,.)

       and

       A4: ( dom G()) = NAT

       and

       A5: (G() . 0 ) = A() & (G() . 1) = B() & (G() . 2) = C() & (G() . 3) = D()

       and

       A6: for n be Nat holds (G() . (n + 4)) = F(n,.,.,.,.);

      defpred Q[ Nat] means (F() . $1) <> (G() . $1);

      assume F() <> G();

      then ex x be object st x in NAT & (F() . x) <> (G() . x) by A1, A4, FUNCT_1: 2;

      then

       A7: ex k be Nat st Q[k];

      consider m be Nat such that

       A8: Q[m] and

       A9: for n be Nat st Q[n] holds m <= n from NAT_1:sch 5( A7);

      now

        set k = (m -' 4);

        

         A10: (F() . (k + 4)) = F(k,.,.,.,.) & (G() . (k + 4)) = F(k,.,.,.,.) by A3, A6;

        assume m <> 0 & ... & m <> 3;

        then 3 < m;

        then (3 + 1) <= m by NAT_1: 13;

        then

         A11: m = (k + 4) by XREAL_1: 235;

        then

         A12: (F() . (k + 1)) = (G() . (k + 1)) by A9, XREAL_1: 6;

        (k + 3) < m by A11, XREAL_1: 6;

        then

         A13: (F() . (k + 3)) = (G() . (k + 3)) by A9;

        (k + 2) < m by A11, XREAL_1: 6;

        then

         A14: (F() . (k + 2)) = (G() . (k + 2)) by A9;

        (k + 0 ) < m by A11, XREAL_1: 6;

        hence contradiction by A8, A9, A11, A12, A14, A13, A10;

      end;

      hence contradiction by A2, A5, A8;

    end;

    scheme :: RECDEF_2:sch13

    LambdaRec4UnD { X() -> non empty set , A,B,C,D() -> Element of X() , F,G() -> sequence of X() , F( object, object, object, object, object) -> Element of X() } :

F() = G()

      provided

       A1: (F() . 0 ) = A() & (F() . 1) = B() & (F() . 2) = C() & (F() . 3) = D()

       and

       A2: for n be Nat holds (F() . (n + 4)) = F(n,.,.,.,.)

       and

       A3: (G() . 0 ) = A() & (G() . 1) = B() & (G() . 2) = C() & (G() . 3) = D()

       and

       A4: for n be Nat holds (G() . (n + 4)) = F(n,.,.,.,.);

      

       A5: ( dom G()) = NAT by FUNCT_2:def 1;

      

       A6: ( dom F()) = NAT by FUNCT_2:def 1;

      thus F() = G() from LambdaRec4Un( A6, A1, A2, A5, A3, A4);

    end;

    begin

    theorem :: RECDEF_2:10

    for x,y,X,Y,Z be set st (x `1_3 ) = (y `1_3 ) & (x `2_3 ) = (y `2_3 ) & (x `3_3 ) = (y `3_3 ) & y in [:X, Y, Z:] & x in [:X, Y, Z:] holds x = y

    proof

      let x,y,X,Y,Z be set;

      assume

       A1: (x `1_3 ) = (y `1_3 ) & (x `2_3 ) = (y `2_3 ) & (x `3_3 ) = (y `3_3 ) & y in [:X, Y, Z:];

      assume x in [:X, Y, Z:];

      

      hence x = [(x `1_3 ), (x `2_3 ), (x `3_3 )] by Th3

      .= y by A1, Th3;

    end;