recdef_1.miz



    begin

    reserve n,m,k for Nat,

D for non empty set,

Z,x,y,z,y1,y2 for set,

p,q for FinSequence;

    

     Lm1: for p be FinSequence of D st 1 <= n & n <= ( len p) holds (p . n) is Element of D

    proof

      let p be FinSequence of D;

      assume 1 <= n & n <= ( len p);

      then n in ( Seg ( len p)) by FINSEQ_1: 1;

      then n in ( dom p) by FINSEQ_1:def 3;

      then

       A1: (p . n) in ( rng p) by FUNCT_1:def 3;

      ( rng p) c= D by FINSEQ_1:def 4;

      hence thesis by A1;

    end;

    definition

      let p be natural-valued Function;

      let n be set;

      :: original: .

      redefine

      func p . n -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    scheme :: RECDEF_1:sch1

    RecEx { A() -> object , P[ object, object, object] } :

ex f be Function st ( dom f) = NAT & (f . 0 ) = A() & for n be Nat holds P[n, (f . n), (f . (n + 1))]

      provided

       A1: for n be Nat holds for x be set holds ex y be set st P[n, x, y];

      defpred Q[ set, set, set] means ex O2 be Ordinal st O2 = $3 & (for X be set, n be Nat st X c= ( Rank ( the_rank_of $2)) holds ex Y be set st Y c= ( Rank O2) & P[n, X, Y]) & (for O be Ordinal st for X be set, n be Nat st X c= ( Rank ( the_rank_of $2)) holds ex Y be set st Y c= ( Rank O) & P[n, X, Y] holds O2 c= O);

      

       A2: for n be Nat holds for x be set holds ex y be set st Q[n, x, y]

      proof

        defpred Y[ object, object] means for m be Nat holds ex y be set st $2 is Ordinal & y c= ( Rank ( the_rank_of $2)) & P[m, $1, y];

        let n be Nat;

        let x be set;

        defpred X[ Ordinal] means for X be set, n be Nat st X c= ( Rank ( the_rank_of x)) holds ex Y be set st Y c= ( Rank $1) & P[n, X, Y];

        

         A3: for x9 be object st x9 in ( bool ( Rank ( the_rank_of x))) holds ex o be object st Y[x9, o]

        proof

          let x9 be object;

          assume x9 in ( bool ( Rank ( the_rank_of x)));

          defpred X[ object, object] means ex y be set st $2 is Ordinal & y c= ( Rank ( the_rank_of $2)) & P[$1, x9, y];

          

           A4: for e be object st e in NAT holds ex u be object st X[e, u]

          proof

            let i be object;

            assume i in NAT ;

            then

            reconsider i9 = i as Nat;

            thus ex o be object, y be set st o is Ordinal & y c= ( Rank ( the_rank_of o)) & P[i, x9, y]

            proof

              x9 is set by TARSKI: 1;

              then

              consider y be set such that

               A5: P[i9, x9, y] by A1;

              take o = ( the_rank_of y), y;

              thus o is Ordinal;

              ( the_rank_of ( the_rank_of y)) = ( the_rank_of y) by CLASSES1: 73;

              hence y c= ( Rank ( the_rank_of o)) by CLASSES1: 65;

              thus thesis by A5;

            end;

          end;

          consider h be Function such that

           A6: ( dom h) = NAT and

           A7: for i be object st i in NAT holds X[i, (h . i)] from CLASSES1:sch 1( A4);

          take o = ( sup ( rng h));

          thus for m be Nat holds ex y be set st o is Ordinal & y c= ( Rank ( the_rank_of o)) & P[m, x9, y]

          proof

            let m be Nat;

            

             A8: m in NAT by ORDINAL1:def 12;

            then

            consider y be set such that

             A9: (h . m) is Ordinal and

             A10: y c= ( Rank ( the_rank_of (h . m))) and

             A11: P[m, x9, y] by A7;

            reconsider O = (h . m) as Ordinal by A9;

            (h . m) in ( rng h) by A6, A8, FUNCT_1:def 3;

            then (h . m) in ( sup ( rng h)) by A9, ORDINAL2: 19;

            then (h . m) c= o by ORDINAL1:def 2;

            then

             A12: ( Rank O) c= ( Rank o) by CLASSES1: 37;

            take y;

            thus o is Ordinal;

            y c= ( Rank O) by A10, CLASSES1: 73;

            then y c= ( Rank o) by A12;

            hence y c= ( Rank ( the_rank_of o)) by CLASSES1: 73;

            thus thesis by A11;

          end;

        end;

        consider f be Function such that

         A13: ( dom f) = ( bool ( Rank ( the_rank_of x))) and

         A14: for x9 be object st x9 in ( bool ( Rank ( the_rank_of x))) holds Y[x9, (f . x9)] from CLASSES1:sch 1( A3);

        

         A15: ex O be Ordinal st X[O]

        proof

          take O2 = ( sup ( rng f));

          thus for X be set, m be Nat st X c= ( Rank ( the_rank_of x)) holds ex Y be set st Y c= ( Rank O2) & P[m, X, Y]

          proof

            let X be set;

            let m be Nat;

            assume

             A16: X c= ( Rank ( the_rank_of x));

            then

            consider Y be set such that

             A17: (f . X) is Ordinal and

             A18: Y c= ( Rank ( the_rank_of (f . X))) and

             A19: P[m, X, Y] by A14;

            reconsider O = (f . X) as Ordinal by A17;

            (f . X) in ( rng f) by A13, A16, FUNCT_1:def 3;

            then (f . X) in ( sup ( rng f)) by A17, ORDINAL2: 19;

            then (f . X) c= O2 by ORDINAL1:def 2;

            then

             A20: ( Rank O) c= ( Rank O2) by CLASSES1: 37;

            take Y;

            ( the_rank_of O) = O by CLASSES1: 73;

            hence Y c= ( Rank O2) by A18, A20;

            thus thesis by A19;

          end;

        end;

        consider O2 be Ordinal such that

         A21: X[O2] & for O be Ordinal st X[O] holds O2 c= O from ORDINAL1:sch 1( A15);

        take O2;

        thus thesis by A21;

      end;

      

       A22: for n be Nat holds for x,y1,y2 be set st Q[n, x, y1] & Q[n, x, y2] holds y1 = y2

      proof

        let n be Nat;

        let x,y1,y2 be set;

        assume that

         A23: Q[n, x, y1] and

         A24: Q[n, x, y2];

        consider O2 be Ordinal such that

         A25: O2 = y2 and

         A26: (for X be set, n be Nat st X c= ( Rank ( the_rank_of x)) holds ex Y be set st Y c= ( Rank O2) & P[n, X, Y]) & for O be Ordinal st for X be set, n be Nat st X c= ( Rank ( the_rank_of x)) holds ex Y be set st Y c= ( Rank O) & P[n, X, Y] holds O2 c= O by A24;

        consider O1 be Ordinal such that

         A27: O1 = y1 and

         A28: (for X be set, n be Nat st X c= ( Rank ( the_rank_of x)) holds ex Y be set st Y c= ( Rank O1) & P[n, X, Y]) & for O be Ordinal st for X be set, n be Nat st X c= ( Rank ( the_rank_of x)) holds ex Y be set st Y c= ( Rank O) & P[n, X, Y] holds O1 c= O by A23;

        O1 c= O2 & O2 c= O1 by A28, A26;

        hence thesis by A27, A25, XBOOLE_0:def 10;

      end;

      ex f be Function st ( dom f) = NAT & (f . 0 ) = ( the_rank_of A()) & for n be Nat holds Q[n, (f . n), (f . (n + 1))]

      proof

        deffunc S( Nat) = { k : k <= $1 };

        

         A29: for p,q be Function, k st ( dom p) = S(k) & ( dom q) = S(+) & (p . 0 ) = (q . 0 ) & for n st n < k holds Q[n, (p . n), (p . (n + 1))] & Q[n, (q . n), (q . (n + 1))] holds (p . k) = (q . k)

        proof

          let p,q be Function;

          let k;

          defpred Z[ Nat] means $1 <= k implies (p . $1) = (q . $1);

          assume that ( dom p) = S(k) and ( dom q) = S(+) and

           A30: (p . 0 ) = (q . 0 ) and

           A31: for n st n < k holds Q[n, (p . n), (p . (n + 1))] & Q[n, (q . n), (q . (n + 1))];

          

           A32: for n st Z[n] holds Z[(n + 1)]

          proof

            let n;

            assume

             A33: n <= k implies (p . n) = (q . n);

            assume (n + 1) <= k;

            then

             A34: n < k by NAT_1: 13;

            then

             A35: Q[n, (p . n), (p . (n + 1))] by A31;

             Q[n, (p . n), (q . (n + 1))] by A31, A33, A34;

            hence thesis by A22, A35;

          end;

          

           A36: Z[ 0 ] by A30;

          for n holds Z[n] from NAT_1:sch 2( A36, A32);

          hence thesis;

        end;

        

         A37: for n holds ex p be Function st ( dom p) = S(n) & (p . 0 ) = ( the_rank_of A()) & for k st k < n holds Q[k, (p . k), (p . (k + 1))]

        proof

          defpred Z[ Nat] means ex p be Function st ( dom p) = S($1) & (p . 0 ) = ( the_rank_of A()) & for k st k < $1 holds Q[k, (p . k), (p . (k + 1))];

          

           A38: for n st Z[n] holds Z[(n + 1)]

          proof

            let n;

            given p be Function such that ( dom p) = S(n) and

             A39: (p . 0 ) = ( the_rank_of A()) and

             A40: for k st k < n holds Q[k, (p . k), (p . (k + 1))];

            consider z such that

             A41: Q[n, (p . n), z] by A2;

            defpred ST[ object, object] means (for k st k = $1 holds (k <= n implies $2 = (p . k)) & (k = (n + 1) implies $2 = z));

            

             A42: for x be object st x in S(+) holds ex y be object st ST[x, y]

            proof

              let x be object;

              assume x in S(+);

              then

               A43: ex m st m = x & m <= (n + 1);

              then

              reconsider t = x as Nat;

              

               A44: t <= n implies thesis

              proof

                assume

                 A45: t <= n;

                take (p . x);

                let k;

                assume

                 A46: k = x;

                hence k <= n implies (p . x) = (p . k);

                assume k = (n + 1);

                then (n + 1) <= (n + 0 ) by A45, A46;

                hence thesis by XREAL_1: 6;

              end;

              t = (n + 1) implies thesis

              proof

                assume

                 A47: t = (n + 1);

                take z;

                let k such that

                 A48: k = x;

                thus k <= n implies z = (p . k)

                proof

                  assume k <= n;

                  then (n + 1) <= (n + 0 ) by A47, A48;

                  hence thesis by XREAL_1: 6;

                end;

                thus thesis;

              end;

              hence thesis by A43, A44, NAT_1: 8;

            end;

            consider q be Function such that

             A49: ( dom q) = S(+) & for x be object st x in S(+) holds ST[x, (q . x)] from CLASSES1:sch 1( A42);

            take q;

            thus ( dom q) = S(+) by A49;

             0 in S(+);

            hence (q . 0 ) = ( the_rank_of A()) by A39, A49;

            let k such that

             A50: k < (n + 1);

             A51:

            now

              

               A52: (k + 1) <= (n + 1) by A50, NAT_1: 13;

              assume k <> n;

              then (k + 1) <> (n + 1);

              then

               A53: (k + 1) <= n by A52, NAT_1: 8;

              then

               A54: k < n by NAT_1: 13;

              (k + 1) in S(+) by A52;

              then

               A55: (q . (k + 1)) = (p . (k + 1)) by A49, A53;

              k in S(+) by A50;

              then (p . k) = (q . k) by A49, A54;

              hence thesis by A40, A55, A54;

            end;

            now

              assume

               A56: k = n;

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

              then k in S(+);

              then

               A57: (q . k) = (p . k) by A49, A56;

              (k + 1) in S(+) by A56;

              then (q . (k + 1)) = z by A49, A56;

              hence thesis by A41, A56, A57;

            end;

            hence thesis by A51;

          end;

          

           A58: Z[ 0 ]

          proof

            set s = ( S(0) --> ( the_rank_of A()));

            take s;

            thus ( dom s) = S(0) by FUNCOP_1: 13;

             0 in S(0);

            hence (s . 0 ) = ( the_rank_of A()) by FUNCOP_1: 7;

            thus thesis;

          end;

          thus for n holds Z[n] from NAT_1:sch 2( A58, A38);

        end;

        ex f be Function st ( dom f) = NAT & for n holds ex p be Function st ( dom p) = S(n) & (p . 0 ) = ( the_rank_of A()) & (for k st k < n holds Q[k, (p . k), (p . (k + 1))]) & (f . n) = (p . n)

        proof

          defpred Z[ object, object] means for n st n = $1 holds ex p be Function st ( dom p) = S(n) & (p . 0 ) = ( the_rank_of A()) & (for k st k < n holds Q[k, (p . k), (p . (k + 1))]) & $2 = (p . n);

          

           A59: for x be object st x in NAT holds ex y be object st Z[x, y]

          proof

            let x be object;

            assume x in NAT ;

            then

            reconsider n = x as Nat;

            consider p be Function such that

             A60: ( dom p) = S(n) & (p . 0 ) = ( the_rank_of A()) & for k st k < n holds Q[k, (p . k), (p . (k + 1))] by A37;

            take (p . n);

            let k such that

             A61: k = x;

            take p;

            thus thesis by A60, A61;

          end;

          consider f be Function such that

           A62: ( dom f) = NAT & for x be object st x in NAT holds Z[x, (f . x)] from CLASSES1:sch 1( A59);

          take f;

          thus ( dom f) = NAT by A62;

          let n;

          n in NAT by ORDINAL1:def 12;

          then

          consider p be Function such that

           A63: ( dom p) = S(n) & (p . 0 ) = ( the_rank_of A()) and

           A64: for k st k < n holds Q[k, (p . k), (p . (k + 1))] and

           A65: (f . n) = (p . n) by A62;

          take p;

          thus ( dom p) = S(n) & (p . 0 ) = ( the_rank_of A()) by A63;

          thus for k st k < n holds Q[k, (p . k), (p . (k + 1))] by A64;

          thus thesis by A65;

        end;

        then

        consider f be Function such that

         A66: ( dom f) = NAT and

         A67: for n holds ex p be Function st ( dom p) = S(n) & (p . 0 ) = ( the_rank_of A()) & (for k st k < n holds Q[k, (p . k), (p . (k + 1))]) & (f . n) = (p . n);

        take f;

        thus ( dom f) = NAT by A66;

        ex p be Function st ( dom p) = S(0) & (p . 0 ) = ( the_rank_of A()) & (for k st k < 0 holds Q[k, (p . k), (p . (k + 1))]) & (f . 0 ) = (p . 0 ) by A67;

        hence (f . 0 ) = ( the_rank_of A());

        let d be Nat;

        consider p be Function such that

         A68: ( dom p) = S(+) and

         A69: (p . 0 ) = ( the_rank_of A()) and

         A70: for k st k < (d + 1) holds Q[k, (p . k), (p . (k + 1))] and

         A71: (f . (d + 1)) = (p . (d + 1)) by A67;

        consider q be Function such that

         A72: ( dom q) = S(d) and

         A73: (q . 0 ) = ( the_rank_of A()) and

         A74: for k st k < d holds Q[k, (q . k), (q . (k + 1))] and

         A75: (f . d) = (q . d) by A67;

        ( dom p) = S(+) & ( dom q) = S(d) & (p . 0 ) = (q . 0 ) & for k st k < d holds Q[k, (q . k), (q . (k + 1))] & Q[k, (p . k), (p . (k + 1))]

        proof

          thus ( dom p) = S(+) by A68;

          thus ( dom q) = S(d) by A72;

          thus (p . 0 ) = (q . 0 ) by A69, A73;

          let k;

          assume

           A76: k < d;

          hence Q[k, (q . k), (q . (k + 1))] by A74;

          d <= (d + 1) by NAT_1: 11;

          then k < (d + 1) by A76, XXREAL_0: 2;

          hence thesis by A70;

        end;

        then (p . d) = (q . d) by A29;

        hence thesis by A70, A71, A75, XREAL_1: 29;

      end;

      then

      consider g be Function such that

       A77: ( dom g) = NAT and

       A78: (g . 0 ) = ( the_rank_of A()) and

       A79: for n be Nat holds Q[n, (g . n), (g . (n + 1))];

      defpred X[ object, object] means ex i be Nat st i = ($1 `2 ) & P[($1 `2 ), ($1 `1 ), ($2 `1 )] & ($2 `2 ) = (i + 1) & not ex y be set st P[($1 `2 ), ($1 `1 ), y] & ( the_rank_of y) in ( the_rank_of ($2 `1 ));

      

       A80: ( [A(), 0 ] `1 ) = A() & ( [A(), 0 ] `2 ) = 0 ;

      set beta = ( sup ( rng g));

      

       A81: for x be object st x in [:( Rank beta), NAT :] holds ex u be object st X[x, u]

      proof

        let x be object;

        defpred X[ Ordinal] means ex y be set st y c= ( Rank $1) & P[(x `2 ), (x `1 ), y];

        assume x in [:( Rank beta), NAT :];

        then

        consider a,b be object such that

         A82: a in ( Rank beta) and

         A83: b in NAT and

         A84: x = [a, b] by ZFMISC_1:def 2;

        reconsider b as Nat by A83;

        

         A85: (x `2 ) = b & (x `1 ) = a by A84;

        ( the_rank_of a) in beta by A82, CLASSES1: 66;

        then

        consider alfa be Ordinal such that

         A86: alfa in ( rng g) and

         A87: ( the_rank_of a) c= alfa by ORDINAL2: 21;

        consider k be object such that

         A88: k in ( dom g) and

         A89: alfa = (g . k) by A86, FUNCT_1:def 3;

        reconsider k as Nat by A77, A88;

        

         A90: Q[k, alfa, (g . (k + 1))] by A79, A89;

        then

        reconsider O2 = (g . (k + 1)) as Ordinal;

        reconsider a as set by TARSKI: 1;

        a c= ( Rank alfa) by A87, CLASSES1: 65;

        then a c= ( Rank ( the_rank_of alfa)) by CLASSES1: 73;

        then ex y be set st y c= ( Rank O2) & P[(x `2 ), (x `1 ), y] by A90, A85;

        then

         A91: ex O be Ordinal st X[O];

        consider O be Ordinal such that

         A92: X[O] and

         A93: for O9 be Ordinal st X[O9] holds O c= O9 from ORDINAL1:sch 1( A91);

        consider Y be set such that

         A94: Y c= ( Rank O) and

         A95: P[b, a, Y] by A85, A92;

        

         A96: ( the_rank_of Y) c= O by A94, CLASSES1: 65;

        take u = [Y, (b + 1)], i = b;

        thus i = (x `2 ) by A84;

        thus P[(x `2 ), (x `1 ), (u `1 )] by A85, A95;

        thus (u `2 ) = (i + 1);

        given y be set such that

         A97: P[(x `2 ), (x `1 ), y] and

         A98: ( the_rank_of y) in ( the_rank_of (u `1 ));

        

         A99: y c= ( Rank ( the_rank_of y)) by CLASSES1:def 9;

        ( the_rank_of y) in ( the_rank_of Y) by A98;

        hence contradiction by A93, A97, A96, A99, ORDINAL1: 5;

      end;

      consider F be Function such that ( dom F) = [:( Rank beta), NAT :] and

       A100: for x be object st x in [:( Rank beta), NAT :] holds X[x, (F . x)] from CLASSES1:sch 1( A81);

      deffunc U( Nat, set) = ((F . [$2, $1]) `1 );

      consider f be Function such that

       A101: ( dom f) = NAT and

       A102: (f . 0 ) = A() and

       A103: for n be Nat holds (f . (n + 1)) = U(n,.) from NAT_1:sch 11;

      defpred X[ Nat] means ( the_rank_of (f . $1)) in ( sup ( rng g));

      (g . 0 ) in ( rng g) by A77, FUNCT_1:def 3;

      then

       A104: X[ 0 ] by A78, A102, ORDINAL2: 19;

      

       A105: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume

         A106: ( the_rank_of (f . n)) in ( sup ( rng g));

        then

        consider o1 be Ordinal such that

         A107: o1 in ( rng g) and

         A108: ( the_rank_of (f . n)) c= o1 by ORDINAL2: 21;

        

         A109: n in NAT by ORDINAL1:def 12;

        (f . n) in ( Rank ( sup ( rng g))) by A106, CLASSES1: 66;

        then

         A110: [(f . n), n] in [:( Rank beta), NAT :] by A109, ZFMISC_1: 87;

        consider m be object such that

         A111: m in ( dom g) and

         A112: (g . m) = o1 by A107, FUNCT_1:def 3;

        reconsider m as Nat by A77, A111;

        consider o2 be Ordinal such that

         A113: o2 = (g . (m + 1)) and

         A114: for X be set, n be Nat st X c= ( Rank ( the_rank_of (g . m))) holds ex Y be set st Y c= ( Rank o2) & P[n, X, Y] and for o be Ordinal st for X be set, n be Nat st X c= ( Rank ( the_rank_of (g . m))) holds ex Y be set st Y c= ( Rank o) & P[n, X, Y] holds o2 c= o by A79;

        ( the_rank_of (f . n)) c= ( the_rank_of (g . m)) by A108, A112, CLASSES1: 73;

        then (f . n) c= ( Rank ( the_rank_of (g . m))) by CLASSES1: 65;

        then

        consider YY be set such that

         A115: YY c= ( Rank o2) and

         A116: P[n, (f . n), YY] by A114;

        

         A117: ( the_rank_of YY) c= o2 by A115, CLASSES1: 65;

        ( [(f . n), n] `1 ) = (f . n) & ( [(f . n), n] `2 ) = n;

        then ex i be Nat st i = n & P[n, (f . n), ((F . [(f . n), n]) `1 )] & ((F . [(f . n), n]) `2 ) = (i + 1) & not ex y be set st P[n, (f . n), y] & ( the_rank_of y) in ( the_rank_of ((F . [(f . n), n]) `1 )) by A100, A110;

        then

         A118: ( the_rank_of ((F . [(f . n), n]) `1 )) c= ( the_rank_of YY) by A116, ORDINAL1: 16;

        (g . (m + 1)) in ( rng g) by A77, FUNCT_1:def 3;

        then

         A119: o2 in ( sup ( rng g)) by A113, ORDINAL2: 19;

        (f . (n + 1)) = ((F . [(f . n), n]) `1 ) by A103;

        hence thesis by A118, A117, A119, ORDINAL1: 12, XBOOLE_1: 1;

      end;

      

       A120: for n be Nat holds X[n] from NAT_1:sch 2( A104, A105);

      defpred X[ Nat] means P[$1, (f . $1), (f . ($1 + 1))];

      

       A121: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume P[n, (f . n), (f . (n + 1))];

        ( the_rank_of (f . (n + 1))) in ( sup ( rng g)) by A120;

        then (f . (n + 1)) in ( Rank ( sup ( rng g))) by CLASSES1: 66;

        then

         A122: [(f . (n + 1)), (n + 1)] in [:( Rank beta), NAT :] by ZFMISC_1: 87;

        ( [(f . (n + 1)), (n + 1)] `1 ) = (f . (n + 1)) & ( [(f . (n + 1)), (n + 1)] `2 ) = (n + 1);

        then ex i be Nat st i = (n + 1) & P[(n + 1), (f . (n + 1)), ((F . [(f . (n + 1)), (n + 1)]) `1 )] & ((F . [(f . (n + 1)), (n + 1)]) `2 ) = (i + 1) & not ex y be set st P[(n + 1), (f . (n + 1)), y] & ( the_rank_of y) in ( the_rank_of ((F . [(f . (n + 1)), (n + 1)]) `1 )) by A100, A122;

        hence thesis by A103;

      end;

      take f;

      thus ( dom f) = NAT by A101;

      thus (f . 0 ) = A() by A102;

      A() in ( Rank ( sup ( rng g))) by A102, A104, CLASSES1: 66;

      then [A(), 0 ] in [:( Rank beta), NAT :] by ZFMISC_1: 87;

      then ex i be Nat st i = ( [A(), 0 ] `2 ) & P[ 0 , A(), ((F . [A(), 0 ]) `1 )] & ((F . [A(), 0 ]) `2 ) = (i + 1) & not ex y be set st P[ 0 , A(), y] & ( the_rank_of y) in ( the_rank_of ((F . [A(), 0 ]) `1 )) by A100, A80;

      then

       A123: X[ 0 ] by A102, A103;

      thus for n be Nat holds X[n] from NAT_1:sch 2( A123, A121);

    end;

    scheme :: RECDEF_1:sch2

    RecExD { D() -> non empty set , A() -> Element of D() , P[ object, object, object] } :

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

      provided

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

      defpred Q[ Nat, set, set] means P[$1, $2, $3];

      

       A2: for x be Element of NAT holds for y be Element of D() holds ex z be Element of D() st Q[x, y, z] by A1;

      consider f be Function of [: NAT , D():], D() such that

       A3: for x be Element of NAT holds for y be Element of D() holds Q[x, y, (f . (x,y))] from BINOP_1:sch 3( A2);

      defpred P[ FinSequence] means (($1 . 1) = A() & for n st (n + 2) <= ( len $1) holds ($1 . (n + 2)) = (f . [n, ($1 . (n + 1))]));

      consider X be set such that

       A4: for x be object holds x in X iff ex p st p in (D() * ) & P[p] & x = p from FINSEQ_1:sch 4;

      set Y = ( union X);

      

       A5: x in X implies x in (D() * )

      proof

        assume x in X;

        then ex p st p in (D() * ) & ((p . 1) = A() & for n st (n + 2) <= ( len p) holds (p . (n + 2)) = (f . [n, (p . (n + 1))])) & x = p by A4;

        hence thesis;

      end;

      

       A6: for p, q st p in X & q in X & ( len p) <= ( len q) holds p c= q

      proof

        let p, q;

        assume that

         A7: p in X and

         A8: q in X and

         A9: ( len p) <= ( len q);

        

         A10: ex q9 be FinSequence st q9 in (D() * ) & ((q9 . 1) = A() & for n st (n + 2) <= ( len q9) holds (q9 . (n + 2)) = (f . [n, (q9 . (n + 1))])) & q = q9 by A4, A8;

        

         A11: ex p9 be FinSequence st p9 in (D() * ) & ((p9 . 1) = A() & for n st (n + 2) <= ( len p9) holds (p9 . (n + 2)) = (f . [n, (p9 . (n + 1))])) & p = p9 by A4, A7;

        

         A12: for n st 1 <= n & n <= ( len p) holds (p . n) = (q . n)

        proof

          defpred P[ Nat] means 1 <= $1 & $1 <= ( len p) & (p . $1) <> (q . $1);

          assume ex n st P[n];

          then

           A13: ex n be Nat st P[n];

          consider k be Nat such that

           A14: P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A13);

          k = 1

          proof

             0 <> k by A14;

            then

            consider n be Nat such that

             A15: k = (n + 1) by NAT_1: 6;

            (n + 0 ) <= (n + 1) by XREAL_1: 7;

            then

             A16: n <= ( len p) by A14, A15, XXREAL_0: 2;

            

             A17: (n + 0 ) < (n + 1) by XREAL_1: 6;

            assume

             A18: k <> 1;

            then 1 < (n + 1) by A14, A15, XXREAL_0: 1;

            then

             A19: 1 <= n by NAT_1: 13;

            n <> 0 by A18, A15;

            then

            consider m be Nat such that

             A20: n = (m + 1) by NAT_1: 6;

            reconsider m as Nat;

            

             A21: (m + 2) <= ( len q) by A9, A14, A15, A20, XXREAL_0: 2;

            (p . k) = (p . (m + (1 + 1))) by A15, A20

            .= (f . [m, (p . n)]) by A11, A14, A15, A20

            .= (f . [m, (q . (m + 1))]) by A14, A15, A19, A16, A17, A20

            .= (q . k) by A10, A15, A20, A21;

            hence thesis by A14;

          end;

          hence contradiction by A11, A10, A14;

        end;

        now

          let x be object;

          assume x in p;

          then

          consider n be Nat such that

           A22: n in ( dom p) and

           A23: x = [n, (p . n)] by FINSEQ_1: 12;

          

           A24: n in ( Seg ( len p)) by A22, FINSEQ_1:def 3;

          then

           A25: 1 <= n by FINSEQ_1: 1;

          

           A26: n <= ( len p) by A24, FINSEQ_1: 1;

          then n <= ( len q) by A9, XXREAL_0: 2;

          then n in ( Seg ( len q)) by A25, FINSEQ_1: 1;

          then

           A27: n in ( dom q) by FINSEQ_1:def 3;

          x = [n, (q . n)] by A12, A23, A25, A26;

          hence x in q by A27, FUNCT_1: 1;

        end;

        hence thesis;

      end;

      

       A28: Y is Function-like

      proof

        let x,y,z be object such that

         A29: [x, y] in Y and

         A30: [x, z] in Y;

        consider Z2 be set such that

         A31: [x, z] in Z2 and

         A32: Z2 in X by A30, TARSKI:def 4;

        Z2 in (D() * ) by A5, A32;

        then

        reconsider q = Z2 as FinSequence of D() by FINSEQ_1:def 11;

        consider Z1 be set such that

         A33: [x, y] in Z1 and

         A34: Z1 in X by A29, TARSKI:def 4;

        Z1 in (D() * ) by A5, A34;

        then

        reconsider p = Z1 as FinSequence of D() by FINSEQ_1:def 11;

        per cases ;

          suppose ( len q) <= ( len p);

          then

           A35: q c= Z1 by A6, A34, A32;

           [x, y] in p by A33;

          hence thesis by A31, A35, FUNCT_1:def 1;

        end;

          suppose ( len p) <= ( len q);

          then p c= Z2 by A6, A34, A32;

          then [x, y] in q by A33;

          hence thesis by A31, FUNCT_1:def 1;

        end;

      end;

      Y is Relation-like

      proof

        let x be object;

        assume x in Y;

        then

        consider Z2 be set such that

         A36: x in Z2 and

         A37: Z2 in X by TARSKI:def 4;

        ex p st p in (D() * ) & P[p] & Z2 = p by A4, A37;

        then Z2 is Relation-like;

        hence ex y,z be object st x = [y, z] by A36;

      end;

      then

      consider g be Function such that

       A38: g = Y by A28;

      

       A39: for x be object st x in ( rng g) holds x in D()

      proof

        let x be object;

        assume x in ( rng g);

        then

        consider y be object such that

         A40: y in ( dom g) & x = (g . y) by FUNCT_1:def 3;

         [y, x] in Y by A38, A40, FUNCT_1: 1;

        then

        consider Z such that

         A41: [y, x] in Z and

         A42: Z in X by TARSKI:def 4;

        Z in (D() * ) by A5, A42;

        then

        reconsider p = Z as FinSequence of D() by FINSEQ_1:def 11;

        y in ( dom p) & x = (p . y) by A41, FUNCT_1: 1;

        then

         A43: x in ( rng p) by FUNCT_1:def 3;

        ( rng p) c= D() by FINSEQ_1:def 4;

        hence thesis by A43;

      end;

      then ( rng g) c= D();

      then

      reconsider h = g as Function of ( dom g), D() by FUNCT_2: 2;

      

       A44: for n holds (n + 1) in ( dom h)

      proof

        defpred P[ Nat] means ($1 + 1) in ( dom h);

        

         A45: for n st (n + 2) <= ( len <*A()*>) holds ( <*A()*> . (n + 2)) = (f . [n, ( <*A()*> . (n + 1))])

        proof

          let n;

          assume (n + 2) <= ( len <*A()*>);

          then (n + 2) <= 1 by FINSEQ_1: 39;

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

          hence thesis by XREAL_1: 6;

        end;

        ( <*A()*> . 1) = A() & <*A()*> in (D() * ) by FINSEQ_1:def 8, FINSEQ_1:def 11;

        then <*A()*> in X by A4, A45;

        then

         A46: { [1, A()]} in X by FINSEQ_1: 37;

        

         A47: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          assume (k + 1) in ( dom h);

          then [(k + 1), (h . (k + 1))] in Y by A38, FUNCT_1: 1;

          then

          consider Z such that

           A48: [(k + 1), (h . (k + 1))] in Z and

           A49: Z in X by TARSKI:def 4;

          Z in (D() * ) by A5, A49;

          then

          reconsider Z as FinSequence of D() by FINSEQ_1:def 11;

          

           A50: (k + 1) = ( len Z) implies thesis

          proof

            set p = (Z ^ <*(f . [k, (Z . (k + 1))])*>);

            

             A51: 1 <= ((k + 1) + 1) by NAT_1: 12;

            assume

             A52: (k + 1) = ( len Z);

            then 1 <= ( len Z) by NAT_1: 12;

            then 1 in ( Seg ( len Z)) by FINSEQ_1: 1;

            then

             A53: 1 in ( dom Z) by FINSEQ_1:def 3;

            

             A54: for n st (n + 2) <= ( len p) holds (p . (n + 2)) = (f . [n, (p . (n + 1))])

            proof

              let n;

              assume (n + 2) <= ( len p);

              then

               A55: (n + 2) <= (( len Z) + ( len <*(f . [k, (Z . (k + 1))])*>)) by FINSEQ_1: 22;

              then

               A56: (n + 2) <= (( len Z) + 1) by FINSEQ_1: 40;

              

               A57: (n + 2) <> (( len Z) + 1) implies thesis

              proof

                ((n + 1) + 1) <= (( len Z) + 1) by A55, FINSEQ_1: 40;

                then 1 <= (n + 1) & (n + 1) <= ( len Z) by NAT_1: 12, XREAL_1: 6;

                then (n + 1) in ( Seg ( len Z)) by FINSEQ_1: 1;

                then

                 A58: (n + 1) in ( dom Z) by FINSEQ_1:def 3;

                

                 A59: 1 <= (n + (1 + 1)) by NAT_1: 12;

                assume

                 A60: (n + 2) <> (( len Z) + 1);

                then (n + 2) <= ( len Z) by A56, NAT_1: 8;

                then (n + 2) in ( Seg ( len Z)) by A59, FINSEQ_1: 1;

                then

                 A61: (n + 2) in ( dom Z) by FINSEQ_1:def 3;

                ex q st q in (D() * ) & (q . 1) = A() & (for n st (n + 2) <= ( len q) holds (q . (n + 2)) = (f . [n, (q . (n + 1))])) & Z = q by A4, A49;

                then (Z . (n + 2)) = (f . [n, (Z . (n + 1))]) by A56, A60, NAT_1: 8;

                then (p . (n + 2)) = (f . [n, (Z . (n + 1))]) by A61, FINSEQ_1:def 7;

                hence thesis by A58, FINSEQ_1:def 7;

              end;

              (n + 2) = (( len Z) + 1) implies thesis

              proof

                ((n + 1) + 1) <= (( len Z) + 1) by A55, FINSEQ_1: 40;

                then 1 <= (n + 1) & (n + 1) <= ( len Z) by NAT_1: 12, XREAL_1: 6;

                then (n + 1) in ( Seg ( len Z)) by FINSEQ_1: 1;

                then

                 A62: (n + 1) in ( dom Z) by FINSEQ_1:def 3;

                assume

                 A63: (n + 2) = (( len Z) + 1);

                

                then (p . (n + 2)) = ( <*(f . [k, (Z . (k + 1))])*> . ((n + 2) - ((n + 2) - 1))) by A55, FINSEQ_1: 23

                .= (f . [n, (Z . (n + 1))]) by A52, A63, FINSEQ_1: 40;

                hence thesis by A62, FINSEQ_1:def 7;

              end;

              hence thesis by A57;

            end;

            

             A64: p in (D() * )

            proof

              1 <= (k + 1) by NAT_1: 12;

              then (k + 1) in ( Seg ( len Z)) by A52, FINSEQ_1: 1;

              then (k + 1) in ( dom Z) by FINSEQ_1:def 3;

              then

               A65: (Z . (k + 1)) in ( rng Z) by FUNCT_1:def 3;

              ( rng Z) c= D() by FINSEQ_1:def 4;

              then

              reconsider z = (Z . (k + 1)) as Element of D() by A65;

              reconsider n = k as Element of NAT by ORDINAL1:def 12;

              p = (Z ^ <*(f . [n, z])*>);

              hence thesis by FINSEQ_1:def 11;

            end;

            ( len p) = (( len Z) + ( len <*(f . [k, (Z . (k + 1))])*>)) by FINSEQ_1: 22

            .= ((k + 1) + 1) by A52, FINSEQ_1: 39;

            then ((k + 1) + 1) in ( Seg ( len p)) by A51, FINSEQ_1: 1;

            then ((k + 1) + 1) in ( dom p) by FINSEQ_1:def 3;

            then

             A66: [((k + 1) + 1), (p . ((k + 1) + 1))] in p by FUNCT_1: 1;

            ex p be FinSequence st p in (D() * ) & (p . 1) = A() & (for n st (n + 2) <= ( len p) holds (p . (n + 2)) = (f . [n, (p . (n + 1))])) & Z = p by A4, A49;

            then (p . 1) = A() by A53, FINSEQ_1:def 7;

            then p in X by A4, A64, A54;

            then [((k + 1) + 1), (p . ((k + 1) + 1))] in h by A38, A66, TARSKI:def 4;

            hence thesis by FUNCT_1: 1;

          end;

          (k + 1) <> ( len Z) implies thesis

          proof

            (k + 1) in ( dom Z) by A48, FUNCT_1: 1;

            then (k + 1) in ( Seg ( len Z)) by FINSEQ_1:def 3;

            then

             A67: (k + 1) <= ( len Z) by FINSEQ_1: 1;

            assume (k + 1) <> ( len Z);

            then (k + 1) < ( len Z) by A67, XXREAL_0: 1;

            then

             A68: ((k + 1) + 1) <= ( len Z) by NAT_1: 13;

            1 <= ((k + 1) + 1) by NAT_1: 12;

            then ((k + 1) + 1) in ( Seg ( len Z)) by A68, FINSEQ_1: 1;

            then ((k + 1) + 1) in ( dom Z) by FINSEQ_1:def 3;

            then [((k + 1) + 1), (Z . ((k + 1) + 1))] in Z by FUNCT_1: 1;

            then [((k + 1) + 1), (Z . ((k + 1) + 1))] in h by A38, A49, TARSKI:def 4;

            hence thesis by FUNCT_1: 1;

          end;

          hence thesis by A50;

        end;

         [1, A()] in { [1, A()]} by TARSKI:def 1;

        then [1, A()] in h by A38, A46, TARSKI:def 4;

        then

         A69: P[ 0 ] by FUNCT_1: 1;

        thus for k holds P[k] from NAT_1:sch 2( A69, A47);

      end;

      

       A70: for n holds (h . (n + 2)) = (f . [n, (h . (n + 1))])

      proof

        let n;

        ((n + 1) + 1) in ( dom h) by A44;

        then [(n + 2), (h . (n + 2))] in h by FUNCT_1:def 2;

        then

        consider Z be set such that

         A71: [(n + 2), (h . (n + 2))] in Z and

         A72: Z in X by A38, TARSKI:def 4;

        

         A73: ex p st p in (D() * ) & ((p . 1) = A() & for n st (n + 2) <= ( len p) holds (p . (n + 2)) = (f . [n, (p . (n + 1))])) & Z = p by A4, A72;

        Z in (D() * ) by A5, A72;

        then

        reconsider Z as FinSequence of D() by FINSEQ_1:def 11;

        (n + 2) in ( dom Z) by A71, FUNCT_1: 1;

        then (n + 2) in ( Seg ( len Z)) by FINSEQ_1:def 3;

        then

         A74: (n + 2) <= ( len Z) by FINSEQ_1: 1;

        (n + 1) <= (n + 2) by XREAL_1: 7;

        then 1 <= (n + 1) & (n + 1) <= ( len Z) by A74, NAT_1: 12, XXREAL_0: 2;

        then (n + 1) in ( Seg ( len Z)) by FINSEQ_1: 1;

        then (n + 1) in ( dom Z) by FINSEQ_1:def 3;

        then [(n + 1), (Z . (n + 1))] in Z by FUNCT_1: 1;

        then

         A75: [(n + 1), (Z . (n + 1))] in h by A38, A72, TARSKI:def 4;

        

        thus (h . (n + 2)) = (Z . (n + 2)) by A71, FUNCT_1: 1

        .= (f . [n, (Z . (n + 1))]) by A73, A74

        .= (f . [n, (h . (n + 1))]) by A75, FUNCT_1: 1;

      end;

      defpred P[ object, object] means ex n st n = $1 & $2 = (h . (n + 1));

      

       A76: for x be object st x in NAT holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider n = x as Nat;

        take (h . (n + 1));

        take n;

        thus thesis;

      end;

      consider g be Function such that

       A77: ( dom g) = NAT & for x be object st x in NAT holds P[x, (g . x)] from CLASSES1:sch 1( A76);

      

       A78: ( dom g) = NAT by A77;

      

       A79: for n holds (g . n) = (h . (n + 1))

      proof

        let n;

        n in NAT by ORDINAL1:def 12;

        then ex m st m = n & (g . n) = (h . (m + 1)) by A77;

        hence thesis;

      end;

      ( rng g) c= D()

      proof

        let x be object;

        assume x in ( rng g);

        then

        consider y be object such that

         A80: y in ( dom g) and

         A81: x = (g . y) by FUNCT_1:def 3;

        reconsider k = y as Nat by A78, A80;

        (k + 1) in ( dom h) by A44;

        then

         A82: (h . (k + 1)) in ( rng h) by FUNCT_1:def 3;

        x = (h . (k + 1)) by A79, A81;

        hence thesis by A39, A82;

      end;

      then

      reconsider g as sequence of D() by A78, FUNCT_2: 2;

      

       A83: for n holds (g . n) = (h . (n + 1)) by A79;

      

       A84: for n st (n + 2) <= ( len <*A()*>) holds ( <*A()*> . (n + 2)) = (f . [n, ( <*A()*> . (n + 1))])

      proof

        let n;

        assume (n + 2) <= ( len <*A()*>);

        then ((n + 1) + 1) <= ( 0 + 1) by FINSEQ_1: 39;

        then (n + 1) <= 0 by XREAL_1: 6;

        then (n + 1) <= ( 0 + n);

        hence thesis by XREAL_1: 6;

      end;

       <*A()*> in (D() * ) & ( <*A()*> . 1) = A() by FINSEQ_1:def 8, FINSEQ_1:def 11;

      then <*A()*> in X by A4, A84;

      then

       A85: { [1, A()]} in X by FINSEQ_1: 37;

      take g;

       [1, A()] in { [1, A()]} by TARSKI:def 1;

      then [1, A()] in h by A38, A85, TARSKI:def 4;

      

      then A() = (h . ( 0 + 1)) by FUNCT_1: 1

      .= (g . 0 ) by A83;

      hence (g . 0 ) = A();

      let n be Nat;

      

       A86: (h . (n + (1 + 1))) = (f . (n,(h . (n + 1)))) by A70;

      

       A87: n in NAT by ORDINAL1:def 12;

      then (g . n) in D() by FUNCT_2: 5;

      then P[n, (g . n), (f . (n,(g . n)))] by A3, A87;

      then P[n, (g . n), (h . ((n + 1) + 1))] by A83, A86;

      hence thesis by A83;

    end;

    

     Lm2: 1 in REAL by NUMBERS: 19;

    scheme :: RECDEF_1:sch3

    FinRecEx { A() -> object , N() -> Nat , P[ object, object, object] } :

ex p be FinSequence st ( len p) = N() & ((p . 1) = A() or N() = 0 ) & for n st 1 <= n & n < N() holds P[n, (p . n), (p . (n + 1))]

      provided

       A1: for n be Nat st 1 <= n & n < N() holds for x be set holds ex y be set st P[n, x, y];

      defpred Q[ Nat, set, set] means ($1 < (N() - 1) implies P[($1 + 1), $2, $3]) & ( not $1 < (N() - 1) implies $3 = 0 );

      

       A2: for n be Nat holds for x be set holds ex y be set st Q[n, x, y]

      proof

        let n be Nat, x be set;

        n < (N() - 1) implies thesis

        proof

          assume

           A3: n < (N() - 1);

          then (n + 1) < N() by XREAL_1: 20;

          then

          consider y such that

           A4: P[(n + 1), x, y] by A1, NAT_1: 11;

          take y;

          thus n < (N() - 1) implies P[(n + 1), x, y] by A4;

          thus thesis by A3;

        end;

        hence thesis;

      end;

      consider f be Function such that

       A5: ( dom f) = NAT & (f . 0 ) = A() & for n be Nat holds Q[n, (f . n), (f . (n + 1))] from RecEx( A2);

      defpred Q[ object, object] means for r be Real st r = $1 holds $2 = (f . (r - 1));

      

       A6: for x be object st x in REAL holds ex y be object st Q[x, y]

      proof

        let x be object;

        assume x in REAL ;

        then

        reconsider r = x as Real;

        take (f . (r - 1));

        thus thesis;

      end;

      consider g be Function such that

       A7: ( dom g) = REAL & for x be object st x in REAL holds Q[x, (g . x)] from CLASSES1:sch 1( A6);

      ( Seg N()) c= REAL by NUMBERS: 19;

      then

       A8: ( dom (g | ( Seg N()))) = ( Seg N()) by A7, RELAT_1: 62;

      then

      reconsider p = (g | ( Seg N())) as FinSequence by FINSEQ_1:def 2;

      take p;

      N() in NAT by ORDINAL1:def 12;

      hence ( len p) = N() by A8, FINSEQ_1:def 3;

      N() <> 0 implies ((p . 1) = A() or N() = 0 )

      proof

        assume N() <> 0 ;

        then

        consider k be Nat such that

         A9: N() = (k + 1) by NAT_1: 6;

        ( 0 + 1) <= (k + 1) by XREAL_1: 7;

        then 1 in ( Seg N()) by A9, FINSEQ_1: 1;

        

        then (p . 1) = (g . 1) by FUNCT_1: 49

        .= (f . (1 - 1)) by A7, Lm2

        .= A() by A5;

        hence thesis;

      end;

      hence (p . 1) = A() or N() = 0 ;

      let n;

      assume that

       A10: 1 <= n and

       A11: n < N();

       0 <> n by A10;

      then

      consider k be Nat such that

       A12: n = (k + 1) by NAT_1: 6;

      

       A13: for n be Nat st n < N() holds (p . (n + 1)) = (f . n)

      proof

        let n be Nat;

        assume n < N();

        then 1 <= (n + 1) & (n + 1) <= N() by NAT_1: 11, NAT_1: 13;

        then

         A14: (n + 1) in ( Seg N()) by FINSEQ_1: 1;

        (n + 1) in REAL by XREAL_0:def 1;

        

        then (g . (n + 1)) = (f . ((n + 1) - 1)) by A7

        .= (f . n);

        hence thesis by A14, FUNCT_1: 49;

      end;

      reconsider k as Nat;

      k <= (k + 1) by NAT_1: 11;

      then

       A15: k < N() by A11, A12, XXREAL_0: 2;

      k < (N() - 1) by A11, A12, XREAL_1: 20;

      then P[(k + 1), (f . k), (f . (k + 1))] by A5;

      then P[(k + 1), (f . k), (p . ((k + 1) + 1))] by A13, A11, A12;

      hence thesis by A13, A12, A15;

    end;

    scheme :: RECDEF_1:sch4

    FinRecExD { D() -> non empty set , A() -> Element of D() , N() -> Nat , P[ object, object, object] } :

ex p be FinSequence of D() st ( len p) = N() & ((p . 1) = A() or N() = 0 ) & for n st 1 <= n & n < N() holds P[n, (p . n), (p . (n + 1))]

      provided

       A1: for n be Nat st 1 <= n & n < N() holds for x be Element of D() holds ex y be Element of D() st P[n, x, y];

      set 00 = the Element of D();

      defpred Z[ Nat, set, set] means ($1 < (N() - 1) implies P[($1 + 1), $2, $3]) & ( not $1 < (N() - 1) implies $3 = 00);

      

       A2: for n be Nat holds for x be Element of D() holds ex y be Element of D() st Z[n, x, y]

      proof

        let n be Nat, x be Element of D();

        n < (N() - 1) implies thesis

        proof

          assume

           A3: n < (N() - 1);

          then (n + 1) < N() by XREAL_1: 20;

          then

          consider y be Element of D() such that

           A4: P[(n + 1), x, y] by A1, NAT_1: 11;

          take y;

          thus n < (N() - 1) implies P[(n + 1), x, y] by A4;

          thus thesis by A3;

        end;

        hence thesis;

      end;

      consider f be sequence of D() such that

       A5: (f . 0 ) = A() & for n be Nat holds Z[n, (f . n), (f . (n + 1))] from RecExD( A2);

      defpred P[ object, object] means for r be Real st r = $1 holds $2 = (f . (r - 1));

      

       A6: for x be object st x in REAL holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in REAL ;

        then

        reconsider r = x as Real;

        take (f . (r - 1));

        thus thesis;

      end;

      consider g be Function such that

       A7: ( dom g) = REAL & for x be object st x in REAL holds P[x, (g . x)] from CLASSES1:sch 1( A6);

      ( Seg N()) c= REAL by NUMBERS: 19;

      then

       A8: ( dom (g | ( Seg N()))) = ( Seg N()) by A7, RELAT_1: 62;

      then

      reconsider p = (g | ( Seg N())) as FinSequence by FINSEQ_1:def 2;

      ( rng p) c= D()

      proof

        let x be object;

        assume x in ( rng p);

        then

        consider y be object such that

         A9: y in ( dom p) and

         A10: x = (p . y) by FUNCT_1:def 3;

        reconsider y as Element of NAT by A9;

        

         A11: (f . (y - 1)) in D()

        proof

          y <> 0 by A8, A9, FINSEQ_1: 1;

          then

          consider k be Nat such that

           A12: y = (k + 1) by NAT_1: 6;

          reconsider k as Element of NAT by ORDINAL1:def 12;

          (f . k) in D();

          hence thesis by A12;

        end;

        

         A13: y in REAL by XREAL_0:def 1;

        (p . y) = (g . y) by A9, FUNCT_1: 47;

        hence thesis by A7, A10, A11, A13;

      end;

      then

      reconsider p as FinSequence of D() by FINSEQ_1:def 4;

      take p;

      N() in NAT by ORDINAL1:def 12;

      hence ( len p) = N() by A8, FINSEQ_1:def 3;

      N() <> 0 implies ((p . 1) = A() or N() = 0 )

      proof

        assume N() <> 0 ;

        then

        consider k be Nat such that

         A14: N() = (k + 1) by NAT_1: 6;

        ( 0 + 1) <= (k + 1) by XREAL_1: 7;

        then 1 in ( Seg N()) by A14, FINSEQ_1: 1;

        

        then (p . 1) = (g . 1) by FUNCT_1: 49

        .= (f . (1 - 1)) by A7, Lm2

        .= A() by A5;

        hence thesis;

      end;

      hence (p . 1) = A() or N() = 0 ;

      let n;

      assume that

       A15: 1 <= n and

       A16: n < N();

       0 <> n by A15;

      then

      consider k be Nat such that

       A17: n = (k + 1) by NAT_1: 6;

      

       A18: for n be Nat st n < N() holds (p . (n + 1)) = (f . n)

      proof

        let n be Nat;

        assume n < N();

        then 1 <= (n + 1) & (n + 1) <= N() by NAT_1: 11, NAT_1: 13;

        then

         A19: (n + 1) in ( Seg N()) by FINSEQ_1: 1;

        (n + 1) in REAL by XREAL_0:def 1;

        

        then (g . (n + 1)) = (f . ((n + 1) - 1)) by A7

        .= (f . n);

        hence thesis by A19, FUNCT_1: 49;

      end;

      reconsider k as Nat;

      k <= (k + 1) by NAT_1: 11;

      then

       A20: k < N() by A16, A17, XXREAL_0: 2;

      k < (N() - 1) by A16, A17, XREAL_1: 20;

      then P[(k + 1), (f . k), (f . (k + 1))] by A5;

      then P[(k + 1), (f . k), (p . ((k + 1) + 1))] by A18, A16, A17;

      hence thesis by A18, A17, A20;

    end;

    scheme :: RECDEF_1:sch5

    SeqBinOpEx { S() -> FinSequence , P[ object, object, object] } :

ex x st ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))]

      provided

       A1: for k, x st 1 <= k & k < ( len S()) holds ex y st P[(S() . (k + 1)), x, y];

      defpred Q[ Nat, set, set] means P[(S() . ($1 + 1)), $2, $3];

      

       A2: for k st 1 <= k & k < ( len S()) holds for x holds ex y st Q[k, x, y] by A1;

      consider p such that

       A3: ( len p) = ( len S()) & ((p . 1) = (S() . 1) or ( len S()) = 0 ) & for k st 1 <= k & k < ( len S()) holds Q[k, (p . k), (p . (k + 1))] from FinRecEx( A2);

      

       A4: ( len S()) <> 0 implies thesis

      proof

        assume

         A5: ( len S()) <> 0 ;

        take (p . ( len p)), p;

        thus (p . ( len p)) = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) by A3, A5;

        let k;

        assume 1 <= k & k < ( len S());

        hence thesis by A3;

      end;

      ( len S()) = 0 implies thesis

      proof

        assume

         A6: ( len S()) = 0 ;

        take (S() . 0 ), S();

        thus (S() . 0 ) = (S() . ( len S())) & ( len S()) = ( len S()) & (S() . 1) = (S() . 1) by A6;

        thus thesis by A6;

      end;

      hence thesis by A4;

    end;

    scheme :: RECDEF_1:sch6

    LambdaSeqBinOpEx { S() -> FinSequence , F( object, object) -> set } :

ex x st ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.);

      defpred P[ object, object, object] means $3 = F($1,$2);

      

       A1: for k, x st 1 <= k & k < ( len S()) holds ex y st P[(S() . (k + 1)), x, y];

      consider x such that

       A2: ex p st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))] from SeqBinOpEx( A1);

      take x;

      consider p such that

       A3: x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) and

       A4: for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.) by A2;

      take p;

      thus x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) by A3;

      let k;

      assume 1 <= k & k < ( len S());

      hence thesis by A4;

    end;

    scheme :: RECDEF_1:sch7

    FinRecUn { A() -> object , N() -> Nat , F,G() -> FinSequence , P[ object, object, object] } :

F() = G()

      provided

       A1: for n st 1 <= n & n < N() holds for x,y1,y2 be set st P[n, x, y1] & P[n, x, y2] holds y1 = y2

       and

       A2: ( len F()) = N() & ((F() . 1) = A() or N() = 0 ) & for n st 1 <= n & n < N() holds P[n, (F() . n), (F() . (n + 1))]

       and

       A3: ( len G()) = N() & ((G() . 1) = A() or N() = 0 ) & for n st 1 <= n & n < N() holds P[n, (G() . n), (G() . (n + 1))];

      defpred P[ Nat] means 1 <= $1 & $1 <= N() & (F() . $1) <> (G() . $1);

      assume

       A4: F() <> G();

      ( dom F()) = ( Seg ( len G())) by A2, A3, FINSEQ_1:def 3

      .= ( dom G()) by FINSEQ_1:def 3;

      then

      consider x be object such that

       A5: x in ( dom F()) and

       A6: (F() . x) <> (G() . x) by A4;

      

       A7: x in ( Seg ( len F())) by A5, FINSEQ_1:def 3;

      reconsider x as Nat by A5;

      

       A8: 1 <= x by A7, FINSEQ_1: 1;

      x <= N() by A2, A7, FINSEQ_1: 1;

      then

       A9: ex n be Nat st P[n] by A6, A8;

      consider n be Nat such that

       A10: P[n] & for k be Nat st P[k] holds n <= k from NAT_1:sch 5( A9);

       0 <> n by A10;

      then

      consider k be Nat such that

       A11: n = (k + 1) by NAT_1: 6;

      reconsider k as Nat;

      n <> 1 by A2, A3, A10;

      then 1 < n by A10, XXREAL_0: 1;

      then

       A12: 1 <= k by A11, NAT_1: 13;

      k < n by A11, XREAL_1: 29;

      then

       A13: k < N() by A10, XXREAL_0: 2;

      n > k by A11, NAT_1: 13;

      then (F() . k) = (G() . k) by A10, A12, A13;

      then

       A14: P[k, (F() . k), (G() . (k + 1))] by A3, A12, A13;

      P[k, (F() . k), (F() . (k + 1))] by A2, A12, A13;

      hence contradiction by A1, A10, A11, A12, A13, A14;

    end;

    scheme :: RECDEF_1:sch8

    FinRecUnD { D() -> non empty set , A() -> Element of D() , N() -> Nat , F,G() -> FinSequence of D() , P[ object, object, object] } :

F() = G()

      provided

       A1: for n st 1 <= n & n < N() holds for x,y1,y2 be Element of D() st P[n, x, y1] & P[n, x, y2] holds y1 = y2

       and

       A2: ( len F()) = N() & ((F() . 1) = A() or N() = 0 ) & for n st 1 <= n & n < N() holds P[n, (F() . n), (F() . (n + 1))]

       and

       A3: ( len G()) = N() & ((G() . 1) = A() or N() = 0 ) & for n st 1 <= n & n < N() holds P[n, (G() . n), (G() . (n + 1))];

      defpred P[ Nat] means 1 <= $1 & $1 <= N() & (F() . $1) <> (G() . $1);

      assume

       A4: F() <> G();

      ( dom F()) = ( Seg ( len G())) by A2, A3, FINSEQ_1:def 3

      .= ( dom G()) by FINSEQ_1:def 3;

      then

      consider x be object such that

       A5: x in ( dom F()) and

       A6: (F() . x) <> (G() . x) by A4;

      

       A7: x in ( Seg ( len F())) by A5, FINSEQ_1:def 3;

      reconsider x as Nat by A5;

      

       A8: 1 <= x by A7, FINSEQ_1: 1;

      x <= N() by A2, A7, FINSEQ_1: 1;

      then

       A9: ex n be Nat st P[n] by A6, A8;

      consider n be Nat such that

       A10: P[n] & for k be Nat st P[k] holds n <= k from NAT_1:sch 5( A9);

       0 <> n by A10;

      then

      consider k be Nat such that

       A11: n = (k + 1) by NAT_1: 6;

      reconsider k as Nat;

      reconsider Gk1 = (G() . (k + 1)) as Element of D() by A3, A10, A11, Lm1;

      n <> 1 by A2, A3, A10;

      then 1 < n by A10, XXREAL_0: 1;

      then

       A12: 1 <= k by A11, NAT_1: 13;

      k < n by A11, XREAL_1: 29;

      then

       A13: k < N() by A10, XXREAL_0: 2;

      then

      reconsider Fk = (F() . k) as Element of D() by A2, A12, Lm1;

      n > k by A11, NAT_1: 13;

      then (F() . k) = (G() . k) by A10, A12, A13;

      then

       A14: P[k, Fk, Gk1] by A3, A12, A13;

      reconsider Fk1 = (F() . (k + 1)) as Element of D() by A2, A10, A11, Lm1;

      P[k, Fk, Fk1] by A2, A12, A13;

      hence contradiction by A1, A10, A11, A12, A13, A14;

    end;

    scheme :: RECDEF_1:sch9

    SeqBinOpUn { S() -> FinSequence , P[ object, object, object], x,y() -> object } :

x() = y()

      provided

       A1: for k, x, y1, y2, z st 1 <= k & k < ( len S()) & z = (S() . (k + 1)) & P[z, x, y1] & P[z, x, y2] holds y1 = y2

       and

       A2: ex p be FinSequence st x() = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))]

       and

       A3: ex p be FinSequence st y() = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))];

      defpred Q[ Nat, set, set] means P[(S() . ($1 + 1)), $2, $3];

      

       A4: for k st 1 <= k & k < ( len S()) holds for x, y1, y2 st Q[k, x, y1] & Q[k, x, y2] holds y1 = y2 by A1;

      consider q such that

       A5: y() = (q . ( len q)) and

       A6: ( len q) = ( len S()) & (q . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds Q[k, (q . k), (q . (k + 1))] by A3;

      

       A7: ( len q) = ( len S()) & ((q . 1) = (S() . 1) or ( len S()) = 0 ) & for k st 1 <= k & k < ( len S()) holds Q[k, (q . k), (q . (k + 1))] by A6;

      consider p such that

       A8: x() = (p . ( len p)) and

       A9: ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds Q[k, (p . k), (p . (k + 1))] by A2;

      

       A10: ( len p) = ( len S()) & ((p . 1) = (S() . 1) or ( len S()) = 0 ) & for k st 1 <= k & k < ( len S()) holds Q[k, (p . k), (p . (k + 1))] by A9;

      p = q from FinRecUn( A4, A10, A7);

      hence thesis by A8, A5;

    end;

    scheme :: RECDEF_1:sch10

    LambdaSeqBinOpUn { S() -> FinSequence , F( object, object) -> object , x,y() -> object } :

x() = y()

      provided

       A1: ex p be FinSequence st x() = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.)

       and

       A2: ex p be FinSequence st y() = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.);

      defpred P[ set, set, set] means $3 = F($1,$2);

      

       A3: ex p st y() = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))] by A2;

      

       A4: for k, x, y1, y2, z st 1 <= k & k < ( len S()) & z = (S() . (k + 1)) & P[z, x, y1] & P[z, x, y2] holds y1 = y2;

      

       A5: ex p st x() = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))] by A1;

      thus x() = y() from SeqBinOpUn( A4, A5, A3);

    end;

    scheme :: RECDEF_1:sch11

    DefRec { A() -> object , n() -> Nat , P[ object, object, object] } :

(ex y be set st ex f be Function st y = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]) & for y1,y2 be set st (ex f be Function st y1 = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]) & (ex f be Function st y2 = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]) holds y1 = y2

      provided

       A1: for n, x holds ex y st P[n, x, y]

       and

       A2: for n, x, y1, y2 st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

      

       A3: for n, x holds ex y st P[n, x, y] by A1;

      consider f be Function such that

       A4: ( dom f) = NAT & (f . 0 ) = A() & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RecEx( A3);

      

       A5: for n be Nat, x, y1, y2 st P[n, x, y1] & P[n, x, y2] holds y1 = y2 by A2;

      thus ex y be set st ex f be Function st y = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]

      proof

        take (f . n()), f;

        thus thesis by A4;

      end;

      let y1,y2 be set;

      given f1 be Function such that

       A6: y1 = (f1 . n()) and

       A7: ( dom f1) = NAT and

       A8: (f1 . 0 ) = A() and

       A9: for n holds P[n, (f1 . n), (f1 . (n + 1))];

      

       A10: for n be Nat holds P[n, (f1 . n), (f1 . (n + 1))] by A9;

      given f2 be Function such that

       A11: y2 = (f2 . n()) and

       A12: ( dom f2) = NAT and

       A13: (f2 . 0 ) = A() and

       A14: for n holds P[n, (f2 . n), (f2 . (n + 1))];

      

       A15: for n be Nat holds P[n, (f2 . n), (f2 . (n + 1))] by A14;

      f1 = f2 from NAT_1:sch 13( A7, A8, A10, A12, A13, A15, A5);

      hence thesis by A6, A11;

    end;

    scheme :: RECDEF_1:sch12

    LambdaDefRec { A() -> object , n() -> Nat , RecFun( object, object) -> set } :

(ex y be set st ex f be Function st y = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds (f . (n + 1)) = RecFun(n,.)) & for y1,y2 be set st (ex f be Function st y1 = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds (f . (n + 1)) = RecFun(n,.)) & (ex f be Function st y2 = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds (f . (n + 1)) = RecFun(n,.)) holds y1 = y2;

      defpred P[ set, set, set] means for z st z = $2 holds $3 = RecFun($1,z);

      

       A1: for n, x holds ex y st P[n, x, y]

      proof

        let n, x;

        take RecFun(n,x);

        thus thesis;

      end;

      

       A2: for n, x, y1, y2 st P[n, x, y1] & P[n, x, y2] holds y1 = y2

      proof

        let n, x, y1, y2;

        assume that

         A3: for z st z = x holds y1 = RecFun(n,z) and

         A4: for z st z = x holds y2 = RecFun(n,z);

        

        thus y1 = RecFun(n,x) by A3

        .= y2 by A4;

      end;

      

       A5: (ex y be set st ex f be Function st y = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]) & for y1,y2 be set st (ex f be Function st y1 = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]) & (ex f be Function st y2 = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]) holds y1 = y2 from DefRec( A1, A2);

      then

      consider y be set, f be Function such that

       A6: y = (f . n()) & ( dom f) = NAT & ((f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]);

      thus ex y be set st ex f be Function st y = (f . n()) & ( dom f) = NAT & (f . 0 ) = A() & for n holds (f . (n + 1)) = RecFun(n,.)

      proof

        take y, f;

        thus thesis by A6;

      end;

      let y1,y2 be set;

      given f1 be Function such that

       A7: y1 = (f1 . n()) & ( dom f1) = NAT & (f1 . 0 ) = A() and

       A8: for n holds (f1 . (n + 1)) = RecFun(n,.);

      

       A9: for n holds P[n, (f1 . n), (f1 . (n + 1))] by A8;

      given f2 be Function such that

       A10: y2 = (f2 . n()) & ( dom f2) = NAT & (f2 . 0 ) = A() and

       A11: for n holds (f2 . (n + 1)) = RecFun(n,.);

      for n holds P[n, (f2 . n), (f2 . (n + 1))] by A11;

      hence thesis by A5, A7, A10, A9;

    end;

    scheme :: RECDEF_1:sch13

    DefRecD { D() -> non empty set , A() -> Element of D() , n() -> Nat , P[ object, object, object] } :

(ex y be Element of D() st ex f be sequence of D() st y = (f . n()) & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]) & for y1,y2 be Element of D() st (ex f be sequence of D() st y1 = (f . n()) & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]) & (ex f be sequence of D() st y2 = (f . n()) & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]) holds y1 = y2

      provided

       A1: for n be Nat, x be Element of D() holds ex y be Element of D() st P[n, x, y]

       and

       A2: for n be Nat, x,y1,y2 be Element of D() st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

      

       A3: for n be Nat, x be Element of D() holds ex y be Element of D() st P[n, x, y] by A1;

      consider f be sequence of D() such that

       A4: (f . 0 ) = A() & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RecExD( A3);

      

       A5: for n be Nat, x,y1,y2 be Element of D() st P[n, x, y1] & P[n, x, y2] holds y1 = y2 by A2;

      thus ex y be Element of D() st ex f be sequence of D() st y = (f . n()) & (f . 0 ) = A() & for n holds P[n, (f . n), (f . (n + 1))]

      proof

        reconsider n = n() as Element of NAT by ORDINAL1:def 12;

        take (f . n), f;

        thus thesis by A4;

      end;

      let y1,y2 be Element of D();

      given f1 be sequence of D() such that

       A6: y1 = (f1 . n()) and

       A7: (f1 . 0 ) = A() and

       A8: for n holds P[n, (f1 . n), (f1 . (n + 1))];

      

       A9: (f1 . 0 ) = A() by A7;

      

       A10: for n be Nat holds P[n, (f1 . n), (f1 . (n + 1))] by A8;

      given f2 be sequence of D() such that

       A11: y2 = (f2 . n()) and

       A12: (f2 . 0 ) = A() and

       A13: for n holds P[n, (f2 . n), (f2 . (n + 1))];

      

       A14: for n be Nat holds P[n, (f2 . n), (f2 . (n + 1))] by A13;

      

       A15: (f2 . 0 ) = A() by A12;

      f1 = f2 from NAT_1:sch 14( A9, A10, A15, A14, A5);

      hence thesis by A6, A11;

    end;

    scheme :: RECDEF_1:sch14

    LambdaDefRecD { D() -> non empty set , A() -> Element of D() , n() -> Nat , RecFun( object, object) -> Element of D() } :

(ex y be Element of D() st ex f be sequence of D() st y = (f . n()) & (f . 0 ) = A() & for n be Nat holds (f . (n + 1)) = RecFun(n,.)) & for y1,y2 be Element of D() st (ex f be sequence of D() st y1 = (f . n()) & (f . 0 ) = A() & for n be Nat holds (f . (n + 1)) = RecFun(n,.)) & (ex f be sequence of D() st y2 = (f . n()) & (f . 0 ) = A() & for n be Nat holds (f . (n + 1)) = RecFun(n,.)) holds y1 = y2;

      defpred Q[ set, set, set] means for z be Element of D() st z = $2 holds $3 = RecFun($1,z);

      

       A1: for n be Nat, x be Element of D() holds ex y be Element of D() st Q[n, x, y]

      proof

        let n be Nat, x be Element of D();

        take RecFun(n,x);

        let z be Element of D();

        assume z = x;

        hence thesis;

      end;

      

       A2: for n be Nat, x,y1,y2 be Element of D() st Q[n, x, y1] & Q[n, x, y2] holds y1 = y2

      proof

        let n be Nat, x,y1,y2 be Element of D();

        assume that

         A3: for z be Element of D() st z = x holds y1 = RecFun(n,z) and

         A4: for z be Element of D() st z = x holds y2 = RecFun(n,z);

        

        thus y1 = RecFun(n,x) by A3

        .= y2 by A4;

      end;

      

       A5: (ex y be Element of D() st ex f be sequence of D() st y = (f . n()) & (f . 0 ) = A() & for n be Nat holds Q[n, (f . n), (f . (n + 1))]) & for y1,y2 be Element of D() st (ex f be sequence of D() st y1 = (f . n()) & (f . 0 ) = A() & for n be Nat holds Q[n, (f . n), (f . (n + 1))]) & (ex f be sequence of D() st y2 = (f . n()) & (f . 0 ) = A() & for n be Nat holds Q[n, (f . n), (f . (n + 1))]) holds y1 = y2 from DefRecD( A1, A2);

      then

      consider y be Element of D(), f be sequence of D() such that

       A6: y = (f . n()) & (f . 0 ) = A() and

       A7: for n be Nat holds Q[n, (f . n), (f . (n + 1))];

      thus ex y be Element of D() st ex f be sequence of D() st y = (f . n()) & (f . 0 ) = A() & for n be Nat holds (f . (n + 1)) = RecFun(n,.)

      proof

        take y, f;

        thus y = (f . n()) & (f . 0 ) = A() by A6;

        let n be Nat;

        reconsider n as Element of NAT by ORDINAL1:def 12;

         Q[n, (f . n), (f . (n + 1))] by A7;

        hence thesis;

      end;

      let y1,y2 be Element of D();

      given f be sequence of D() such that

       A8: y1 = (f . n()) & (f . 0 ) = A() and

       A9: for n be Nat holds (f . (n + 1)) = RecFun(n,.);

      

       A10: for n be Nat holds Q[n, (f . n), (f . (n + 1))] by A9;

      given f2 be sequence of D() such that

       A11: y2 = (f2 . n()) & (f2 . 0 ) = A() and

       A12: for n be Nat holds (f2 . (n + 1)) = RecFun(n,.);

      for n be Nat holds Q[n, (f2 . n), (f2 . (n + 1))] by A12;

      hence thesis by A5, A8, A11, A10;

    end;

    scheme :: RECDEF_1:sch15

    SeqBinOpDef { S() -> FinSequence , P[ object, object, object] } :

(ex x st ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))]) & for x, y st (ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))]) & (ex p be FinSequence st y = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))]) holds x = y

      provided

       A1: for k, y st 1 <= k & k < ( len S()) holds ex z st P[(S() . (k + 1)), y, z]

       and

       A2: for k, x, y1, y2, z st 1 <= k & k < ( len S()) & z = (S() . (k + 1)) & P[z, x, y1] & P[z, x, y2] holds y1 = y2;

      

       A3: for k, x, y1, y2, z st 1 <= k & k < ( len S()) & z = (S() . (k + 1)) & P[z, x, y1] & P[z, x, y2] holds y1 = y2 by A2;

      

       A4: for k, y st 1 <= k & k < ( len S()) holds ex z st P[(S() . (k + 1)), y, z] by A1;

      thus ex x st ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))] from SeqBinOpEx( A4);

      let x, y;

      assume

       A5: ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))];

      assume

       A6: ex p be FinSequence st y = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds P[(S() . (k + 1)), (p . k), (p . (k + 1))];

      thus x = y from SeqBinOpUn( A3, A5, A6);

    end;

    scheme :: RECDEF_1:sch16

    LambdaSeqBinOpDef { S() -> FinSequence , F( object, object) -> set } :

(ex x st ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.)) & for x, y st (ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.)) & (ex p be FinSequence st y = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.)) holds x = y;

      thus ex x st ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.) from LambdaSeqBinOpEx;

      let x, y;

      assume

       A1: ex p be FinSequence st x = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.);

      assume

       A2: ex p be FinSequence st y = (p . ( len p)) & ( len p) = ( len S()) & (p . 1) = (S() . 1) & for k st 1 <= k & k < ( len S()) holds (p . (k + 1)) = F(.,.);

      thus x = y from LambdaSeqBinOpUn( A1, A2);

    end;

    scheme :: RECDEF_1:sch17

    SeqExD { D() -> non empty set , N() -> Nat , P[ object, object] } :

ex p be FinSequence of D() st ( dom p) = ( Seg N()) & for k be Nat st k in ( Seg N()) holds P[k, (p /. k)]

      provided

       A1: for k be Nat st k in ( Seg N()) holds ex x be Element of D() st P[k, x];

      per cases ;

        suppose

         A2: N() = 0 ;

        take ( <*> D());

        thus thesis by A2;

      end;

        suppose

         A3: N() <> 0 ;

        now

          assume

           A4: ( Seg N()) = {} ;

          now

            per cases ;

              case N() = 0 ;

              hence contradiction by A3;

            end;

              case N() <> 0 ;

              hence contradiction by A4;

            end;

          end;

          hence contradiction;

        end;

        then

        reconsider M = ( Seg N()) as non empty set;

        

         A5: for x be Element of M holds ex y be Element of D() st P[x, y]

        proof

          let x be Element of M;

          x in ( Seg N());

          hence thesis by A1;

        end;

        consider f be Function of M, D() such that

         A6: for x be Element of M holds P[x, (f . x)] from FUNCT_2:sch 3( A5);

        ( dom f) = ( Seg N()) by FUNCT_2:def 1;

        then

        reconsider q = f as FinSequence by FINSEQ_1:def 2;

        now

          let u be object;

          

           A7: ( rng q) c= D() by RELAT_1:def 19;

          assume u in ( rng q);

          hence u in D() by A7;

        end;

        then ( rng q) c= D();

        then

        reconsider q as FinSequence of D() by FINSEQ_1:def 4;

        take q;

        now

          let k be Nat;

          assume

           A8: k in ( Seg N());

          then k in ( dom q) by FUNCT_2:def 1;

          then (q . k) = (q /. k) by PARTFUN1:def 6;

          hence P[k, (q /. k)] by A6, A8;

        end;

        hence thesis by FUNCT_2:def 1;

      end;

    end;

    scheme :: RECDEF_1:sch18

    FinRecExD2 { D() -> non empty set , A() -> Element of D() , N() -> Element of NAT , P[ object, object, object] } :

ex p be FinSequence of D() st ( len p) = N() & ((p /. 1) = A() or N() = 0 ) & for n be Nat st 1 <= n & n <= (N() - 1) holds P[n, (p /. n), (p /. (n + 1))]

      provided

       A1: for n be Nat st 1 <= n & n <= (N() - 1) holds for x be Element of D() holds ex y be Element of D() st P[n, x, y];

      set 00 = the Element of D();

      defpred Q[ Nat, set, set] means ( 0 <= $1 & $1 <= (N() - 2) implies P[($1 + 1), $2, $3]) & ( not ( 0 <= $1 & $1 <= (N() - 2)) implies $3 = 00);

      

       A2: for n be Nat holds for x be Element of D() holds ex y be Element of D() st Q[n, x, y]

      proof

        let n be Nat, x be Element of D();

         0 <= n & n <= (N() - 2) implies thesis

        proof

          

           A3: ( 0 + 1) <= (n + 1) by XREAL_1: 6;

          assume that 0 <= n and

           A4: n <= (N() - 2);

          (n + 1) <= ((N() - 2) + 1) by A4, XREAL_1: 6;

          then

          consider y be Element of D() such that

           A5: P[(n + 1), x, y] by A1, A3;

          take y;

          thus 0 <= n & n <= (N() - 2) implies P[(n + 1), x, y] by A5;

          thus thesis by A4;

        end;

        hence thesis;

      end;

      consider f be sequence of D() such that

       A6: (f . 0 ) = A() & for n be Nat holds Q[n, (f . n), (f . (n + 1))] from RecExD( A2);

      defpred Q[ object, object] means for r be Real st r = $1 holds $2 = (f . (r - 1));

      

       A7: for x be object st x in REAL holds ex y be object st Q[x, y]

      proof

        let x be object;

        assume x in REAL ;

        then

        reconsider r = x as Real;

        take (f . (r - 1));

        thus thesis;

      end;

      consider g be Function such that

       A8: ( dom g) = REAL & for x be object st x in REAL holds Q[x, (g . x)] from CLASSES1:sch 1( A7);

      ( Seg N()) c= REAL by NUMBERS: 19;

      then

       A9: ( dom (g | ( Seg N()))) = ( Seg N()) by A8, RELAT_1: 62;

      then

      reconsider p = (g | ( Seg N())) as FinSequence by FINSEQ_1:def 2;

      now

        let x be object;

        assume x in ( rng p);

        then

        consider y be object such that

         A10: y in ( dom p) and

         A11: x = (p . y) by FUNCT_1:def 3;

        reconsider y as Element of NAT by A10;

        

         A12: (f . (y - 1)) in D()

        proof

          y <> 0 by A9, A10, FINSEQ_1: 1;

          then

          consider k be Nat such that

           A13: y = (k + 1) by NAT_1: 6;

          reconsider k as Element of NAT by ORDINAL1:def 12;

          (f . k) in D();

          hence thesis by A13;

        end;

        

         A14: y in REAL by XREAL_0:def 1;

        (p . y) = (g . y) by A10, FUNCT_1: 47;

        hence x in D() by A8, A11, A12, A14;

      end;

      then ( rng p) c= D();

      then

      reconsider p as FinSequence of D() by FINSEQ_1:def 4;

      take p;

      thus ( len p) = N() by A9, FINSEQ_1:def 3;

      N() <> 0 implies (p /. 1) = A()

      proof

        assume N() <> 0 ;

        then

        consider k be Nat such that

         A15: N() = (k + 1) by NAT_1: 6;

        ( 0 + 1) <= (k + 1) by XREAL_1: 7;

        then

         A16: 1 in ( Seg N()) by A15, FINSEQ_1: 1;

        

        then (p /. 1) = (p . 1) by A9, PARTFUN1:def 6

        .= (g . 1) by A16, FUNCT_1: 49

        .= (f . (1 - 1)) by A8, Lm2

        .= A() by A6;

        hence thesis;

      end;

      hence (p /. 1) = A() or N() = 0 ;

      let n be Nat;

      assume that

       A17: 1 <= n and

       A18: n <= (N() - 1);

      consider k be Nat such that

       A19: n = (k + 1) by A17, NAT_1: 6;

      

       A20: for n be Nat st n <= (N() - 1) holds (p /. (n + 1)) = (f . n)

      proof

        let n be Nat;

        assume n <= (N() - 1);

        then

         A21: (n + 1) <= ((N() - 1) + 1) by XREAL_1: 6;

        (n + 1) in REAL by XREAL_0:def 1;

        

        then

         A22: (g . (n + 1)) = (f . ((n + 1) - 1)) by A8

        .= (f . n);

        1 <= (n + 1) by NAT_1: 11;

        then

         A23: (n + 1) in ( Seg N()) by A21, FINSEQ_1: 1;

        then (p /. (n + 1)) = (p . (n + 1)) by A9, PARTFUN1:def 6;

        hence thesis by A23, A22, FUNCT_1: 49;

      end;

      

       A24: k <= (k + 1) by NAT_1: 11;

      k <= ((N() - 1) - 1) by A18, A19, XREAL_1: 19;

      then P[(k + 1), (f . k), (f . (k + 1))] by A6;

      then P[(k + 1), (f . k), (p /. ((k + 1) + 1))] by A20, A18, A19;

      hence thesis by A20, A18, A19, A24, XXREAL_0: 2;

    end;