stirl2_1.miz

    begin

    reserve k,l,m,n,i,j for Nat,

K,N for non empty Subset of NAT ,

Ke,Ne,Me for Subset of NAT ,

X,Y for set;

    theorem :: STIRL2_1:1



     Th1: ( min N) = ( min* N)

    proof



       A1: for n be ExtReal st n in N holds ( min* N) <= n by NAT_1:def 1;

      ( min* N) in N by NAT_1:def 1;

      hence thesis by A1, XXREAL_2:def 7;

    end;

    theorem :: STIRL2_1:2



     Th2: ( min (( min K),( min N))) = ( min (K \/ N))

    proof

      set m = ( min (( min N),( min K)));



       A1: for k be ExtReal st k in (N \/ K) holds m <= k

      proof

        let k be ExtReal;

        assume k in (N \/ K);

        then k in N or k in K by XBOOLE_0:def 3;

        then

         A2: ( min N) <= k or ( min K) <= k by XXREAL_2:def 7;



         A3: m <= ( min K) by XXREAL_0: 17;

        m <= ( min N) by XXREAL_0: 17;

        hence thesis by A2, A3, XXREAL_0: 2;

      end;

      m = ( min N) or m = ( min K) by XXREAL_0: 15;

      then m in N or m in K by XXREAL_2:def 7;

      then m in (N \/ K) by XBOOLE_0:def 3;

      hence thesis by A1, XXREAL_2:def 7;

    end;

    theorem :: STIRL2_1:3

    ( min (( min* Ke),( min* Ne))) <= ( min* (Ke \/ Ne))

    proof

      now

        per cases ;

          suppose Ke is empty or Ne is empty;

          then ( min* Ke) = 0 & ( min* Ne) >= 0 or ( min* Ne) = 0 & ( min* Ke) >= 0 by NAT_1:def 1;

          hence thesis by XXREAL_0:def 9;

        end;

          suppose Ke is non empty & Ne is non empty;

          then

          reconsider K = Ke, N = Ne as non empty Subset of NAT ;



           A1: ( min N) = ( min* Ne) by Th1;



           A2: ( min (K \/ N)) = ( min* (Ke \/ Ne)) by Th1;

          ( min K) = ( min* Ke) by Th1;

          hence thesis by A1, A2, Th2;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:4

     not ( min* Ne) in (Ne /\ Ke) implies ( min* Ne) = ( min* (Ne \ Ke))

    proof

      assume

       A1: not ( min* Ne) in (Ne /\ Ke);

      now

        per cases ;

          suppose Ne is empty;

          hence thesis;

        end;

          suppose Ne is non empty;

          then

           A2: ( min* Ne) in Ne by NAT_1:def 1;

          then not ( min* Ne) in Ke by A1, XBOOLE_0:def 4;

          then

           A3: ( min* Ne) in (Ne \ Ke) by A2, XBOOLE_0:def 5;

          then

           A4: ( min* (Ne \ Ke)) <= ( min* Ne) by NAT_1:def 1;



           A5: (Ne \ Ke) c= Ne by XBOOLE_1: 36;

          ( min* (Ne \ Ke)) in (Ne \ Ke) by A3, NAT_1:def 1;

          then ( min* Ne) <= ( min* (Ne \ Ke)) by A5, NAT_1:def 1;

          hence thesis by A4, XXREAL_0: 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:5



     Th5: for n be Element of NAT holds ( min* {n}) = n & ( min {n}) = n

    proof

      let n be Element of NAT ;



       A1: ( min* {n}) in {n} by NAT_1:def 1;

      ( min* {n}) = ( min {n}) by Th1;

      hence thesis by A1, TARSKI:def 1;

    end;

    theorem :: STIRL2_1:6



     Th6: for n,k be Element of NAT holds ( min* {n, k}) = ( min (n,k)) & ( min {n, k}) = ( min (n,k))

    proof

      let n,k be Element of NAT ;



       A1: ( min {n}) = n by Th5;

       {n, k} = ( {n} \/ {k}) by ENUMSET1: 1;

      then

       A2: ( min {n, k}) = ( min (( min {n}),( min {k}))) by Th2;

      ( min {n, k}) = ( min* {n, k}) by Th1;

      hence thesis by A2, A1, Th5;

    end;

    theorem :: STIRL2_1:7

    for n,k,l be Element of NAT holds ( min* {n, k, l}) = ( min (n,( min (k,l))))

    proof

      let n,k,l be Element of NAT ;



       A1: ( min {n, k, l}) = ( min* {n, k, l}) by Th1;

       {n, k, l} = ( {n} \/ {k, l}) by ENUMSET1: 2;

      then

       A2: ( min {n, k, l}) = ( min (( min {n}),( min {k, l}))) by Th2;

      ( min {k, l}) = ( min (k,l)) by Th6;

      hence thesis by A2, A1, Th5;

    end;

    theorem :: STIRL2_1:8



     Th8: n is Subset of NAT

    proof

      now

        let x be object;

        assume x in { l where l be Nat : l < n };

        then ex l be Nat st x = l & l < n;

        hence x in NAT by ORDINAL1:def 12;

      end;

      then { l where l be Nat : l < n } c= NAT ;

      hence thesis by AXIOMS: 4;

    end;

    registration

      let n;

      cluster -> natural for Element of ( Segm n);

      coherence ;

    end

    theorem :: STIRL2_1:9

    N c= n implies (n - 1) is Element of NAT

    proof



       A1: ( min* N) in N by NAT_1:def 1;

      assume N c= n;

      then ( min* N) in n by A1;

      then ( min* N) in { l where l be Nat : l < n } by AXIOMS: 4;

      then ex l be Nat st ( min* N) = l & l < n;

      hence thesis by NAT_1: 20;

    end;

    theorem :: STIRL2_1:10



     Th10: k in ( Segm n) implies k <= (n - 1) & (n - 1) is Element of NAT

    proof

      assume k in ( Segm n);

      then k in { l where l be Nat : l < n } by AXIOMS: 4;

      then

       A1: ex l be Nat st k = l & l < n;

      then

       A2: (n - 1) is Element of NAT by NAT_1: 20;

      k < ((n - 1) + 1) by A1;

      hence thesis by A2, NAT_1: 13;

    end;

    theorem :: STIRL2_1:11

    ( min* n) = 0

    proof

      now

        per cases ;

          suppose 0 = n;

          hence thesis by NAT_1:def 1;

        end;

          suppose 0 < n;

          then 0 in { l where l be Nat : l < n };

          then

           A1: 0 in n by AXIOMS: 4;

          n is Subset of NAT by Th8;

          hence thesis by A1, NAT_1:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:12



     Th12: N c= ( Segm n) implies ( min* N) <= (n - 1)

    proof



       A1: ( min* N) in N by NAT_1:def 1;

      assume N c= ( Segm n);

      hence thesis by A1, Th10;

    end;

    theorem :: STIRL2_1:13

    N c= ( Segm n) & N <> {(n - 1)} implies ( min* N) < (n - 1)

    proof

      assume that

       A1: N c= ( Segm n) and

       A2: N <> {(n - 1)} and

       A3: ( min* N) >= (n - 1);

      now

        let k be object such that

         A4: k in N;

        reconsider k9 = k as Element of NAT by A4;

        ( min* N) <= k9 by A4, NAT_1:def 1;

        then

         A5: (n - 1) <= k9 by A3, XXREAL_0: 2;

        k9 <= (n - 1) by A1, A4, Th10;

        then (n - 1) = k by A5, XXREAL_0: 1;

        hence k in {(n - 1)} by TARSKI:def 1;

      end;

      then N c= {(n - 1)};

      hence thesis by A2, ZFMISC_1: 33;

    end;

    theorem :: STIRL2_1:14



     Th14: Ne c= ( Segm n) & n > 0 implies ( min* Ne) <= (n - 1)

    proof

      assume that

       A1: Ne c= ( Segm n) and

       A2: n > 0 ;

      now

        per cases ;

          suppose Ne is non empty;

          hence thesis by A1, Th12;

        end;

          suppose Ne is empty;

          then ( min* Ne) = 0 by NAT_1:def 1;

          hence thesis by A2, NAT_1: 20;

        end;

      end;

      hence thesis;

    end;

    reserve f for Function of ( Segm n), ( Segm k);

    definition

      let n, X;

      let f be Function of ( Segm n), X;

      let x be set;

      :: original: "

      redefine

      func f " x -> Subset of NAT ;

      coherence

      proof

        for y be object st y in (f " x) holds y in NAT by TARSKI:def 3;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let X, k;

      let f be Function of X, ( Segm k);

      let x be object;

      :: original: .

      redefine

      func f . x -> Element of ( Segm k) ;

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

          then (f . x) in ( rng f) by FUNCT_1: 3;

          hence (f . x) is Element of ( Segm k);

        end;

          suppose

           A1: not x in ( dom f);



           A2: k = 0 or k > 0 ;

          (f . x) = 0 by A1, FUNCT_1:def 2;

          hence thesis by A2, NAT_1: 44, SUBSET_1:def 1;

        end;

      end;

    end

    definition

      let n,k be Nat;

      let f be Function of ( Segm n), ( Segm k);

      :: STIRL2_1:def1

      attr f is "increasing means (n = 0 iff k = 0 ) & for l, m st l in ( rng f) & m in ( rng f) & l < m holds ( min* (f " {l})) < ( min* (f " {m}));

    end

    theorem :: STIRL2_1:15



     Th15: n = 0 & k = 0 implies f is onto "increasing

    proof

      assume that

       A1: n = 0 and

       A2: k = 0 ;

      ( rng f) = {} by A1;

      hence thesis by A1, A2, FUNCT_2:def 3;

    end;

    theorem :: STIRL2_1:16



     Th16: n > 0 implies ( min* (f " {m})) <= (n - 1)

    proof



       A1: (f " {m}) c= n

      proof

        let x be object;

        assume x in (f " {m});

        then x in ( dom f) by FUNCT_1:def 7;

        hence thesis;

      end;

      assume n > 0 ;

      hence thesis by A1, Th14;

    end;

    theorem :: STIRL2_1:17



     Th17: f is onto implies n >= k

    proof

      assume

       A1: f is onto;

      now

        per cases ;

          suppose k = 0 ;

          hence thesis;

        end;

          suppose

           A2: k <> 0 ;



           A3: ( rng f) = k by A1, FUNCT_2:def 3;

          ( dom f) = n by A2, FUNCT_2:def 1;

          then ( Segm ( card k)) c= ( Segm ( card n)) by A3, CARD_1: 12;

          then

           A4: ( card k) <= ( card n) by NAT_1: 39;

          thus thesis by A4;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:18



     Th18: f is onto "increasing implies for m st m < k holds m <= ( min* (f " {m}))

    proof

      defpred M[ Nat] means $1 < k implies $1 <= ( min* (f " {$1}));

      assume that

       A1: f is onto "increasing;



       A2: for m st M[m] holds M[(m + 1)]

      proof



         A3: k = ( rng f) by A1, FUNCT_2:def 3;

        let m such that

         A4: M[m];

        assume

         A5: (m + 1) < k;

        m < (m + 1) by NAT_1: 19;

        then m < k by A5, XXREAL_0: 2;

        then

         A6: m in ( rng f) by A3, NAT_1: 44;



         A7: m < (m + 1) by NAT_1: 19;

        (m + 1) in ( rng f) by A5, A3, NAT_1: 44;

        then ( min* (f " {m})) < ( min* (f " {(m + 1)})) by A1, A6, A7;

        then m < ( min* (f " {(m + 1)})) by A4, A5, A7, XXREAL_0: 2;

        hence thesis by NAT_1: 13;

      end;



       A8: M[ 0 ];

      for m holds M[m] from NAT_1:sch 2( A8, A2);

      hence thesis;

    end;

    theorem :: STIRL2_1:19



     Th19: f is onto "increasing implies for m st m < k holds ( min* (f " {m})) <= ((n - k) + m)

    proof

      assume that

       A1: f is onto "increasing;

      now

        per cases ;

          suppose k = 0 ;

          hence thesis;

        end;

          suppose k > 0 ;

          then

          reconsider k1 = (k - 1) as Element of NAT by NAT_1: 20;

          defpred I[ Integer] means 0 <= $1 implies ( min* (f " {$1})) <= ((n - k) + $1);



           A2: k1 < (k1 + 1) by NAT_1: 13;



           A3: for m be Integer st m <= k1 holds I[m] implies I[(m - 1)]

          proof

            reconsider nk = (n - k) as Element of NAT by A1, Th17, NAT_1: 21;



             A4: k = ( rng f) by A1, FUNCT_2:def 3;

            let m be Integer;

            assume m <= k1;

            then

             A5: m < k by A2, XXREAL_0: 2;

            assume

             A6: I[m];

            assume 0 <= (m - 1);

            then

            reconsider m1 = (m - 1) as Element of NAT by INT_1: 3;



             A7: m1 < (m1 + 1) by NAT_1: 19;

            then m1 < k by A5, XXREAL_0: 2;

            then

             A8: m1 in ( Segm k) by NAT_1: 44;

            (m1 + 1) in ( Segm k) by A5, NAT_1: 44;

            then ( min* (f " {m1})) < ( min* (f " {(m1 + 1)})) by A1, A7, A8, A4;

            then ( min* (f " {m1})) < ((nk + m1) + 1) by A6, XXREAL_0: 2;

            hence thesis by NAT_1: 13;

          end;



           A9: I[k1]

          proof

            assume 0 <= k1;

            k = 0 iff n = 0 by A1;

            then ( min* (f " {k1})) <= (n - 1) by Th16;

            hence thesis;

          end;



           A10: for m be Integer st m <= k1 holds I[m] from INT_1:sch 3( A9, A3);

          now

            let m;

            assume m < k;

            then m < (k1 + 1);

            then m <= k1 by NAT_1: 13;

            hence ( min* (f " {m})) <= ((n - k) + m) by A10;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:20



     Th20: f is onto "increasing & n = k implies f = ( id n)

    proof

      assume that

       A1: f is onto "increasing and

       A2: n = k;

      now

        per cases ;

          suppose

           A3: n = 0 ;

          thus thesis by A3;

        end;

          suppose

           A4: n > 0 ;

           A5:

          now

            let m9 be object such that

             A6: m9 in ( Segm n);

            reconsider m = m9 as Element of NAT by A6;

            m in ( rng f) by A1, A2, A6, FUNCT_2:def 3;

            then

             A7: ex x be object st x in ( dom f) & (f . x) = m by FUNCT_1:def 3;

            m in {m} by TARSKI:def 1;

            then

            reconsider F = (f " {m}) as non empty Subset of NAT by A7, FUNCT_1:def 7;



             A8: m < k by A2, A6, NAT_1: 44;

            then

             A9: m <= ( min* (f " {m})) by A1, Th18;

            ((n - k) + m) = m by A2;

            then ( min* (f " {m})) <= m by A1, A8, Th19;

            then

             A10: ( min* F) = m by A9, XXREAL_0: 1;

            ( min* F) in F by NAT_1:def 1;

            then (f . m) in {m} by A10, FUNCT_1:def 7;

            hence (f . m9) = m9 by TARSKI:def 1;

          end;

          ( dom f) = n by A2, A4, FUNCT_2:def 1;

          hence thesis by A5, FUNCT_1: 17;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:21

    f = ( id n) & n > 0 implies f is "increasing

    proof

      assume that

       A1: f = ( id n) and

       A2: n > 0 ;



       A3: ex x be object st x in n by A2, XBOOLE_0:def 1;

       A4:

      now

        let l, m such that

         A5: l in ( rng f) and

         A6: m in ( rng f) and

         A7: l < m;



         A8: ex x be object st (f " {l}) = {x} by A1, A5, FUNCT_1: 74;



         A9: l in {l} by TARSKI:def 1;

        consider l9 be object such that

         A10: l9 in ( dom f) and

         A11: (f . l9) = l by A5, FUNCT_1:def 3;

        l = l9 by A1, A10, A11, FUNCT_1: 18;

        then l in (f " {l}) by A10, A11, A9, FUNCT_1:def 7;

        then (f " {l}) = {l} & l in NAT by A8, TARSKI:def 1;

        then

         A12: ( min* (f " {l})) = l by Th5;



         A13: m in {m} by TARSKI:def 1;



         A14: ex x be object st (f " {m}) = {x} by A1, A6, FUNCT_1: 74;

        consider m9 be object such that

         A15: m9 in ( dom f) and

         A16: (f . m9) = m by A6, FUNCT_1:def 3;

        m = m9 by A1, A15, A16, FUNCT_1: 18;

        then m in (f " {m}) by A15, A16, A13, FUNCT_1:def 7;

        then (f " {m}) = {m} & m in NAT by A14, TARSKI:def 1;

        hence ( min* (f " {l})) < ( min* (f " {m})) by A7, A12, Th5;

      end;

      ( rng f) = n by A1;

      hence thesis by A3, A4;

    end;

    theorem :: STIRL2_1:22

    (n = 0 iff k = 0 ) implies ex f be Function of ( Segm n), ( Segm k) st f is "increasing

    proof

      assume

       A1: n = 0 iff k = 0 ;

      now

        per cases ;

          suppose

           A2: n = 0 ;

          set f = {} ;



           A3: ( dom f) = n by A2;

          ( rng f) = k by A1, A2;

          then

          reconsider f as Function of ( Segm n), ( Segm k) by A3, FUNCT_2: 1;

          f is "increasing by A1;

          hence thesis;

        end;

          suppose n > 0 ;

          then

          consider f be Function such that

           A4: ( dom f) = n and

           A5: ( rng f) = { 0 } by FUNCT_1: 5;

          reconsider f as Function of n, { 0 } by A4, A5, FUNCT_2: 1;

          ( rng f) c= ( Segm k)

          proof

            let x be object such that

             A6: x in ( rng f);

            x = 0 by A6, TARSKI:def 1;

            hence thesis by A1, A6, NAT_1: 44;

          end;

          then

          reconsider f as Function of ( Segm n), ( Segm k) by FUNCT_2: 6;

          for l, m st l in ( rng f) & m in ( rng f) & l < m holds ( min* (f " {l})) < ( min* (f " {m})) by A5, TARSKI:def 1;

          then f is "increasing by A1;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:23



     Th23: (n = 0 iff k = 0 ) & n >= k implies ex f be Function of ( Segm n), ( Segm k) st f is onto "increasing

    proof

      assume that

       A1: n = 0 iff k = 0 and

       A2: n >= k;

      now

        per cases ;

          suppose

           A3: n = 0 ;

          set f = {} ;



           A4: ( dom f) = n by A3;

          ( rng f) = k by A1, A3;

          then

          reconsider f as Function of ( Segm n), ( Segm k) by A4, FUNCT_2: 1;

          f is onto "increasing by A1, Th15;

          hence thesis;

        end;

          suppose

           A5: n > 0 ;

          then

          reconsider k1 = (k - 1) as Element of NAT by A1, NAT_1: 20;

          reconsider k, n as non zero Element of NAT by A1, A5, ORDINAL1:def 12;

          defpred F[ Element of ( Segm n), Element of ( Segm k)] means $2 = ( min ($1,k1));



           A6: for x be Element of ( Segm n) holds ex y be Element of ( Segm k) st F[x, y]

          proof

            let x be Element of ( Segm n);



             A7: k1 < (k1 + 1) by NAT_1: 13;

            ( min (x,k1)) <= k1 by XXREAL_0: 17;

            then ( min (x,k1)) < k by A7, XXREAL_0: 2;

            then ( min (x,k1)) in ( Segm k) by NAT_1: 44;

            hence thesis;

          end;

          consider f be Function of ( Segm n), ( Segm k) such that

           A8: for m be Element of ( Segm n) holds F[m, (f . m) qua Element of ( Segm k)] from FUNCT_2:sch 3( A6);

          now

            let m9 be object such that

             A9: m9 in ( Segm k);

            reconsider m = m9 as Element of NAT by A9;



             A10: m < (k1 + 1) by A9, NAT_1: 44;

            then m < n by A2, XXREAL_0: 2;

            then

             A11: m in ( Segm n) by NAT_1: 44;

            then

             A12: m in ( dom f) by FUNCT_2:def 1;

            m <= k1 by A10, NAT_1: 13;

            then ( min (m,k1)) = m by XXREAL_0:def 9;

            then (f . m) = m by A8, A11;

            hence m9 in ( rng f) by A12, FUNCT_1:def 3;

          end;

          then k c= ( rng f);

          then k = ( rng f);

          then

           A13: f is onto by FUNCT_2:def 3;



           A14: for m st m in ( rng f) holds ( min* (f " {m})) = m

          proof

            let m;

            assume m in ( rng f);

            then

             A15: m < (k1 + 1) by NAT_1: 44;

            then

             A16: m <= k1 by NAT_1: 13;

            m < n by A2, A15, XXREAL_0: 2;

            then

             A17: m in ( Segm n) by NAT_1: 44;

            then

             A18: m in ( dom f) by FUNCT_2:def 1;

            m <= k1 by A15, NAT_1: 13;

            then ( min (m,k1)) = m by XXREAL_0:def 9;

            then (f . m) = m by A8, A17;

            then

             A19: (f . m) in {m} by TARSKI:def 1;

            then

             A20: m in (f " {m}) by A18, FUNCT_1:def 7;



             A21: (f " {m}) is non empty by A19, A18, FUNCT_1:def 7;

            now

              per cases by A16, XXREAL_0: 1;

                suppose

                 A22: m < k1;

                now



                   A23: n is Subset of NAT by Th8;

                  let l9 be object such that

                   A24: l9 in (f " {m});

                  l9 in ( dom f) by A24, FUNCT_1:def 7;

                  then l9 in n;

                  then

                  reconsider l = l9 as Element of NAT by A23;

                  (f . l) in {m} by A24, FUNCT_1:def 7;

                  then

                   A25: (f . l) = m by TARSKI:def 1;

                  l in ( dom f) by A24, FUNCT_1:def 7;

                  then ( min (l,k1)) = m by A8, A25;

                  then l = m by A22, XXREAL_0: 15;

                  hence l9 in {m} by TARSKI:def 1;

                end;

                then

                 A26: (f " {m}) c= {m};

                ( min* (f " {m})) in (f " {m}) by A21, NAT_1:def 1;

                hence thesis by A26, TARSKI:def 1;

              end;

                suppose

                 A27: m = k1;

                for l be Nat st l in (f " {m}) holds m <= l

                proof

                  let l be Nat such that

                   A28: l in (f " {m});

                  (f . l) in {m} by A28, FUNCT_1:def 7;

                  then

                   A29: (f . l) = m by TARSKI:def 1;

                  l in ( dom f) by A28, FUNCT_1:def 7;

                  then (f . l) = ( min (l,m)) by A8, A27;

                  hence thesis by A29, XXREAL_0:def 9;

                end;

                hence thesis by A20, NAT_1:def 1;

              end;

            end;

            hence thesis;

          end;

          now

            let l, m such that

             A30: l in ( rng f) and

             A31: m in ( rng f) and

             A32: l < m;

            ( min* (f " {l})) = l by A14, A30;

            hence ( min* (f " {l})) < ( min* (f " {m})) by A14, A31, A32;

          end;

          then f is "increasing;

          hence thesis by A13;

        end;

      end;

      hence thesis;

    end;

    scheme :: STIRL2_1:sch1

    Sch1 { n,k() -> Nat , P[ set] } :

{ f where f be Function of ( Segm n()), ( Segm k()) : P[f] } is finite;

      set F = { f where f be Function of ( Segm n()), ( Segm k()) : P[f] };

      now

        per cases ;

          suppose

           A1: k() = 0 ;

          F c= { {} }

          proof

            let x be object;

            assume x in F;

            then

            consider f be Function of n(), k() such that

             A2: x = f and P[f];

            f = {} by A1;

            hence thesis by A2, TARSKI:def 1;

          end;

          hence thesis;

        end;

          suppose

           A3: k() > 0 ;



           A4: F c= ( Funcs (n(),k()))

          proof

            let x be object;

            assume x in F;

            then ex f be Function of n(), k() st x = f & P[f];

            hence thesis by A3, FUNCT_2: 8;

          end;

          ( Funcs (n(),k())) is finite by FRAENKEL: 6;

          hence thesis by A4;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:24



     Th24: for n, k holds { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing } is finite

    proof

      let n, k;

      defpred P[ Function of ( Segm n), ( Segm k)] means $1 is onto "increasing;

      { f where f be Function of ( Segm n), ( Segm k) : P[f] } is finite from Sch1;

      hence thesis;

    end;

    theorem :: STIRL2_1:25



     Th25: for n, k holds ( card { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing }) is Element of NAT

    proof

      let n, k;

      set F = { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing };

      F is finite by Th24;

      then

      reconsider m = ( card F) as Nat;

      ( card F) = ( card m);

      hence thesis;

    end;

    definition

      let n,k be Nat;

      :: STIRL2_1:def2

      func n block k -> set equals ( card { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing });

      coherence ;

    end

    registration

      let n,k be Nat;

      cluster (n block k) -> natural;

      coherence by Th25;

    end

    theorem :: STIRL2_1:26



     Th26: (n block n) = 1

    proof

      set F = { f where f be Function of ( Segm n), ( Segm n) : f is onto "increasing };



       A1: F c= {( id n)}

      proof

        let x be object;

        assume x in F;

        then

        consider f be Function of ( Segm n), ( Segm n) such that

         A2: x = f and

         A3: f is onto "increasing;

        f = ( id n) by A3, Th20;

        hence thesis by A2, TARSKI:def 1;

      end;

      n = 0 iff n = 0 ;

      then

      consider f be Function of ( Segm n), ( Segm n) such that

       A4: f is onto "increasing by Th23;

      f in F by A4;

      then F = {( id n)} by A1, ZFMISC_1: 33;

      hence thesis by CARD_1: 30;

    end;

    theorem :: STIRL2_1:27



     Th27: k <> 0 implies ( 0 block k) = 0

    proof

      set F = { f where f be Function of ( Segm 0 ), ( Segm k) : f is onto "increasing };

      assume

       A1: k <> 0 ;

      F = {}

      proof

        assume F <> {} ;

        then

        consider x be object such that

         A2: x in F by XBOOLE_0:def 1;

        ex f be Function of ( Segm 0 ), ( Segm k) st x = f & f is onto "increasing by A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:28

    ( 0 block k) = 1 iff k = 0 by Th26, Th27;

    theorem :: STIRL2_1:29



     Th29: n < k implies (n block k) = 0

    proof

      set F = { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing };

      assume

       A1: n < k;

      F = {}

      proof

        assume F <> {} ;

        then

        consider x be object such that

         A2: x in F by XBOOLE_0:def 1;

        ex f be Function of ( Segm n), ( Segm k) st x = f & f is onto "increasing by A2;

        hence contradiction by A1, Th17;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:30

    (n block 0 ) = 1 iff n = 0

    proof

      (n block 0 ) = 1 implies n = 0

      proof

        set F = { f where f be Function of ( Segm n), ( Segm 0 ) : f is onto "increasing };



         A1: ( card { {} }) = 1 by CARD_1: 30;

        assume (n block 0 ) = 1;

        then

        consider x be object such that

         A2: F = {x} by A1, CARD_1: 29;

        x in F by A2, TARSKI:def 1;

        then ex f be Function of ( Segm n), ( Segm 0 ) st x = f & f is onto "increasing;

        hence thesis;

      end;

      hence thesis by Th26;

    end;

    theorem :: STIRL2_1:31



     Th31: n <> 0 implies (n block 0 ) = 0

    proof

      set F = { f where f be Function of ( Segm n), ( Segm 0 ) : f is onto "increasing };

      assume

       A1: n <> 0 ;

      F = {}

      proof

        assume F <> {} ;

        then

        consider x be object such that

         A2: x in F by XBOOLE_0:def 1;

        ex f be Function of ( Segm n), ( Segm 0 ) st x = f & f is onto "increasing by A2;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:32



     Th32: n <> 0 implies (n block 1) = 1

    proof

      set F = { g where g be Function of ( Segm n), ( Segm 1) : g is onto "increasing };

      assume n <> 0 ;

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

      then

      consider f be Function of ( Segm n), ( Segm 1) such that

       A1: f is onto "increasing by Th23;



       A2: F c= {f}

      proof

        let x be object;

        assume x in F;

        then

        consider g be Function of ( Segm n), ( Segm 1) such that

         A3: x = g and g is onto "increasing;

        f = g by CARD_1: 49, FUNCT_2: 51;

        hence thesis by A3, TARSKI:def 1;

      end;

      f in F by A1;

      then F = {f} by A2, ZFMISC_1: 33;

      hence thesis by CARD_1: 30;

    end;

    theorem :: STIRL2_1:33

    1 <= k & k <= n or k = n iff (n block k) qua Nat > 0

    proof

      thus 1 <= k & k <= n or k = n implies (n block k) > 0

      proof

        set F = { g where g be Function of ( Segm n), ( Segm k) : g is onto "increasing };

        assume that

         A1: 1 <= k & k <= n or k = n;

        k = 0 iff n = 0 by A1;

        then

        consider f such that

         A2: f is onto "increasing by A1, Th23;

        f in F by A2;

        hence thesis;

      end;

      thus (n block k) > 0 implies 1 <= k & k <= n or k = n

      proof

        assume

         A3: (n block k) > 0 ;

        assume

         A4: not (1 <= k & k <= n or k = n);

        then (1 + 0 ) > k or k > n;

        then k = 0 & n <> k or k > n by A4, NAT_1: 13;

        hence contradiction by A3, Th29, Th31;

      end;

    end;

    reserve x,y for set;

    scheme :: STIRL2_1:sch2

    Sch2 { X,Y,X1,Y1() -> set , f() -> Function of X(), Y() , F( object) -> object } :

ex h be Function of X1(), Y1() st (h | X()) = f() & for x st x in (X1() \ X()) holds (h . x) = F(x)

      provided

       A1: for x st x in (X1() \ X()) holds F(x) in Y1()

       and

       A2: X() c= X1() & Y() c= Y1()

       and

       A3: Y() is empty implies X() is empty;

      defpred P[ object, object] means ($1 in X() implies $2 = (f() . $1)) & ($1 in (X1() \ X()) implies $2 = F($1));



       A4: for x be object st x in X1() holds ex y be object st y in Y1() & P[x, y]

      proof

        let x be object such that

         A5: x in X1();

        now

          per cases ;

            suppose

             A6: x in X();

            then x in ( dom f()) by A3, FUNCT_2:def 1;

            then (f() . x) in ( rng f()) by FUNCT_1:def 3;

            then

             A7: (f() . x) in Y1() by A2;

             not x in (X1() \ X()) by A6, XBOOLE_0:def 5;

            hence thesis by A7;

          end;

            suppose

             A8: not x in X();

            then x in (X1() \ X()) by A5, XBOOLE_0:def 5;

            then F(x) in Y1() by A1;

            hence thesis by A8;

          end;

        end;

        hence thesis;

      end;

      consider h be Function of X1(), Y1() such that

       A9: for x be object st x in X1() holds P[x, (h . x)] from FUNCT_2:sch 1( A4);



       A10: ( dom f()) = (( dom h) /\ X())

      proof

        now

          per cases ;

            suppose Y() is empty;

            hence thesis by A3;

          end;

            suppose

             A11: Y() is non empty;

            then Y1() is non empty by A2;

            then

             A12: ( dom h) = X1() by FUNCT_2:def 1;

            ( dom f()) = X() by A11, FUNCT_2:def 1;

            hence thesis by A2, A12, XBOOLE_1: 28;

          end;

        end;

        hence thesis;

      end;

      take h;

      for x be object st x in ( dom f()) holds (h . x) = (f() . x)

      proof

        let x be object;

        assume x in ( dom f());

        then x in X();

        hence thesis by A2, A9;

      end;

      hence (h | X()) = f() by A10, FUNCT_1: 46;

      thus thesis by A9;

    end;

    scheme :: STIRL2_1:sch3

    Sch3 { X,Y,X1,Y1() -> set , F( object) -> object , P[ set, set, set] } :

( card { f where f be Function of X(), Y() : P[f, X(), Y()] }) = ( card { f where f be Function of X1(), Y1() : P[f, X1(), Y1()] & ( rng (f | X())) c= Y() & (for x st x in (X1() \ X()) holds (f . x) = F(x)) })

      provided

       A1: for x st x in (X1() \ X()) holds F(x) in Y1()

       and

       A2: X() c= X1() & Y() c= Y1()

       and

       A3: Y() is empty implies X() is empty

       and

       A4: for f be Function of X1(), Y1() st (for x st x in (X1() \ X()) holds F(x) = (f . x)) holds P[f, X1(), Y1()] iff P[(f | X()), X(), Y()];

      defpred FF[ object, object] means for f be Function of X(), Y(), h be Function of X1(), Y1() st f = $1 & h = $2 holds (h | X()) = f;

      set F2 = { f where f be Function of X1(), Y1() : P[f, X1(), Y1()] & ( rng (f | X())) c= Y() & for x st x in (X1() \ X()) holds (f . x) = F(x) };

      set F1 = { f where f be Function of X(), Y() : P[f, X(), Y()] };



       A5: for f9 be object st f9 in F1 holds ex g9 be object st g9 in F2 & FF[f9, g9]

      proof

        let f9 be object;

        assume f9 in F1;

        then

        consider f be Function of X(), Y() such that

         A6: f = f9 and

         A7: P[f, X(), Y()];

        consider h be Function of X1(), Y1() such that

         A8: (h | X()) = f & for x st x in (X1() \ X()) holds (h . x) = F(x) from Sch2( A1, A2, A3);



         A9: FF[f9, h] by A6, A8;



         A10: ( rng f) c= Y();

        P[h, X1(), Y1()] by A4, A7, A8;

        then h in F2 by A8, A10;

        hence thesis by A9;

      end;

      consider ff be Function of F1, F2 such that

       A11: for x be object st x in F1 holds FF[x, (ff . x)] from FUNCT_2:sch 1( A5);



       A12: Y1() is empty implies X1() is empty by A1, A2, A3;

      now

        per cases ;

          suppose

           A13: Y1() is empty;

          set Empty = {} ;



           A14: F2 c= { {} }

          proof

            let x be object;

            assume x in F2;

            then ex f be Function of X1(), Y1() st f = x & P[f, X1(), Y1()] & ( rng (f | X())) c= Y() & for x st x in (X1() \ X()) holds (f . x) = F(x);

            then x = {} by A13;

            hence thesis by TARSKI:def 1;

          end;



           A15: F1 c= { {} }

          proof

            let x be object;

            assume x in F1;

            then ex f be Function of X(), Y() st f = x & P[f, X(), Y()];

            then x = {} by A2, A13;

            hence thesis by TARSKI:def 1;

          end;

          now

            per cases ;

              suppose

               A16: P[ {} , {} , {} ];



               A17: ( rng {} ) = {} ;



               A18: Y() is empty by A2, A13;

               {} is Function of X(), Y() by A3, A18, A17, FUNCT_2: 1;

              then {} in F1 by A3, A16, A18;

              then

               A19: F1 = { {} } by A15, ZFMISC_1: 33;



               A20: ( rng {} ) = {} ;

              reconsider Empty as Function of X1(), Y1() by A12, A13, A20, FUNCT_2: 1;



               A21: for x st x in (X1() \ X()) holds (Empty . x) = F(x) by A12;

              ( rng (Empty | X())) c= Y();

              then {} in F2 by A12, A13, A16, A21;

              hence thesis by A14, A19, ZFMISC_1: 33;

            end;

              suppose

               A22: not P[ {} , {} , {} ];



               A23: not {} in F1

              proof

                assume {} in F1;

                then ex f be Function of X(), Y() st f = {} & P[f, X(), Y()];

                hence contradiction by A2, A3, A13, A22;

              end;



               A24: F2 = {} or F2 = { {} } by A14, ZFMISC_1: 33;



               A25: not {} in F2

              proof

                assume {} in F2;

                then ex f be Function of X1(), Y1() st f = {} & P[f, X1(), Y1()] & ( rng (f | X())) c= Y() & for x st x in (X1() \ X()) holds (f . x) = F(x);

                hence contradiction by A12, A13, A22;

              end;

              F1 = {} or F1 = { {} } by A15, ZFMISC_1: 33;

              hence thesis by A23, A25, A24, TARSKI:def 1;

            end;

          end;

          hence thesis;

        end;

          suppose

           A26: Y1() is non empty;

          now

            per cases ;

              suppose

               A27: F2 is empty;

              F1 is empty

              proof

                assume F1 is non empty;

                then

                consider x be object such that

                 A28: x in F1;

                consider f be Function of X(), Y() such that f = x and

                 A29: P[f, X(), Y()] by A28;



                 A30: ( rng f) c= Y();

                consider h be Function of X1(), Y1() such that

                 A31: (h | X()) = f & for x st x in (X1() \ X()) holds (h . x) = F(x) from Sch2( A1, A2, A3);

                P[h, X1(), Y1()] by A4, A29, A31;

                then h in F2 by A31, A30;

                hence thesis by A27;

              end;

              hence thesis by A27;

            end;

              suppose

               A32: F2 is non empty;

              F2 c= ( rng ff)

              proof

                let y be object;

                assume y in F2;

                then

                consider f be Function of X1(), Y1() such that

                 A33: f = y and

                 A34: P[f, X1(), Y1()] and

                 A35: ( rng (f | X())) c= Y() and

                 A36: for x st x in (X1() \ X()) holds (f . x) = F(x);



                 A37: ( dom (f | X())) = (( dom f) /\ X()) by RELAT_1: 61;

                ( dom f) = X1() by A26, FUNCT_2:def 1;

                then

                 A38: ( dom (f | X())) = X() by A2, A37, XBOOLE_1: 28;

                then

                reconsider h = (f | X()) as Function of X(), ( rng (f | X())) by FUNCT_2: 1;

                ( rng (f | X())) is empty implies X() is empty by A38, RELAT_1: 42;

                then

                reconsider h as Function of X(), Y() by A35, FUNCT_2: 6;

                P[(f | X()), X(), Y()] by A4, A34, A36;

                then

                 A39: h in F1;



                 A40: ( dom ff) = F1 by A32, FUNCT_2:def 1;

                then (ff . h) in ( rng ff) by A39, FUNCT_1:def 3;

                then (ff . h) in F2;

                then

                consider ffh be Function of X1(), Y1() such that

                 A41: ffh = (ff . h) and P[ffh, X1(), Y1()] and ( rng (ffh | X())) c= Y() and

                 A42: for x st x in (X1() \ X()) holds (ffh . x) = F(x);

                now

                  let x be object such that

                   A43: x in X1();

                  now

                    per cases ;

                      suppose x in X();

                      then

                       A44: x in ( dom h) by A3, FUNCT_2:def 1;

                      (ffh | X()) = h by A11, A39, A41;

                      then (h . x) = (ffh . x) by A44, FUNCT_1: 47;

                      hence (ffh . x) = (f . x) by A44, FUNCT_1: 47;

                    end;

                      suppose not x in X();

                      then

                       A45: x in (X1() \ X()) by A43, XBOOLE_0:def 5;

                      then (ffh . x) = F(x) by A42;

                      hence (ffh . x) = (f . x) by A36, A45;

                    end;

                  end;

                  hence (ffh . x) = (f . x);

                end;

                then ffh = f by FUNCT_2: 12;

                hence thesis by A33, A39, A40, A41, FUNCT_1:def 3;

              end;

              then

               A46: ( rng ff) = F2;

              for x1,x2 be object st x1 in F1 & x2 in F1 & (ff . x1) = (ff . x2) holds x1 = x2

              proof

                let x1,x2 be object such that

                 A47: x1 in F1 and

                 A48: x2 in F1 and

                 A49: (ff . x1) = (ff . x2);



                 A50: ex f2 be Function of X(), Y() st x2 = f2 & P[f2, X(), Y()] by A48;

                ( dom ff) = F1 by A32, FUNCT_2:def 1;

                then (ff . x1) in ( rng ff) by A47, FUNCT_1:def 3;

                then (ff . x1) in F2;

                then

                consider F1 be Function of X1(), Y1() such that

                 A51: (ff . x1) = F1 and P[F1, X1(), Y1()] and ( rng (F1 | X())) c= Y() and for x st x in (X1() \ X()) holds (F1 . x) = F(x);

                consider f1 be Function of X(), Y() such that

                 A52: x1 = f1 and P[f1, X(), Y()] by A47;

                (F1 | X()) = f1 by A11, A47, A52, A51;

                hence thesis by A11, A48, A49, A52, A50, A51;

              end;

              then

               A53: ff is one-to-one by A32, FUNCT_2: 19;

              ( dom ff) = F1 by A32, FUNCT_2:def 1;

              then (F1,F2) are_equipotent by A46, A53, WELLORD2:def 4;

              hence thesis by CARD_1: 5;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    scheme :: STIRL2_1:sch4

    Sch4 { X,Y() -> set , x,y() -> object , P[ set, set, set] } :

( card { f where f be Function of X(), Y() : P[f, X(), Y()] }) = ( card { f where f be Function of (X() \/ {x()}), (Y() \/ {y()}) : P[f, (X() \/ {x()}), (Y() \/ {y()})] & ( rng (f | X())) c= Y() & (f . x()) = y() })

      provided

       A1: Y() is empty implies X() is empty

       and

       A2: not x() in X()

       and

       A3: for f be Function of (X() \/ {x()}), (Y() \/ {y()}) st (f . x()) = y() holds P[f, (X() \/ {x()}), (Y() \/ {y()})] iff P[(f | X()), X(), Y()];

      set Y1 = (Y() \/ {y()});

      set X1 = (X() \/ {x()});

      deffunc F( set) = y();



       A4: for f be Function of X1, Y1 holds (for x st x in (X1 \ X()) holds F(x) = (f . x)) iff (f . x()) = y()

      proof

        let f be Function of X1, Y1;



         A5: (X1 \ X()) = ( {x()} \ X()) by XBOOLE_1: 40

        .= {x()} by A2, ZFMISC_1: 59;

        thus (for x st x in (X1 \ X()) holds F(x) = (f . x)) implies (f . x()) = y()

        proof



           A6: x() in {x()} by TARSKI:def 1;

          assume for x st x in (X1 \ X()) holds F(x) = (f . x);

          hence thesis by A5, A6;

        end;

        thus thesis by A5, TARSKI:def 1;

      end;



       A7: for f be Function of X1, Y1 st (for x st x in (X1 \ X()) holds F(x) = (f . x)) holds P[f, X1, Y1] iff P[(f | X()), X(), Y()]

      proof

        let f be Function of X1, Y1;

        assume for x st x in (X1 \ X()) holds F(x) = (f . x);

        then y() = (f . x()) by A4;

        hence thesis by A3;

      end;

      set F2 = { f where f be Function of X1, Y1 : P[f, X1, Y1] & ( rng (f | X())) c= Y() & (f . x()) = y() };

      set F1 = { f where f be Function of X1, Y1 : P[f, X1, Y1] & ( rng (f | X())) c= Y() & for x st x in (X1 \ X()) holds (f . x) = F(x) };



       A8: for x st x in (X1 \ X()) holds F(x) in Y1

      proof

        let x such that x in (X1 \ X());



         A9: {y()} c= Y1 by XBOOLE_1: 7;

        y() in {y()} by TARSKI:def 1;

        hence thesis by A9;

      end;



       A10: F1 c= F2

      proof

        let x be object;

        assume x in F1;

        then

        consider f be Function of X1, Y1 such that

         A11: x = f and

         A12: P[f, X1, Y1] and

         A13: ( rng (f | X())) c= Y() and

         A14: for x st x in (X1 \ X()) holds (f . x) = F(x);

        (f . x()) = y() by A4, A14;

        hence thesis by A11, A12, A13;

      end;



       A15: F2 c= F1

      proof

        let x be object;

        assume x in F2;

        then

        consider f be Function of X1, Y1 such that

         A16: x = f and

         A17: P[f, X1, Y1] and

         A18: ( rng (f | X())) c= Y() and

         A19: (f . x()) = y();

        for x st x in (X1 \ X()) holds F(x) = (f . x) by A4, A19;

        hence thesis by A16, A17, A18;

      end;



       A20: X() c= X1 & Y() c= Y1 by XBOOLE_1: 7;

      ( card { f where f be Function of X(), Y() : P[f, X(), Y()] }) = ( card F1) from Sch3( A8, A20, A1, A7);

      hence thesis by A10, A15, XBOOLE_0:def 10;

    end;

    theorem :: STIRL2_1:34



     Th34: for f be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f is onto "increasing & (f " {(f . n)}) = {n} holds (f . n) = k

    proof

      let f be Function of ( Segm (n + 1)), ( Segm (k + 1)) such that

       A1: f is onto "increasing and

       A2: (f " {(f . n)}) = {n};

      assume

       A3: (f . n) <> k;

      now

        per cases by A3, XXREAL_0: 1;

          suppose

           A4: (f . n) > k;

          (f . n) < (k + 1) by NAT_1: 44;

          hence contradiction by A4, NAT_1: 13;

        end;

          suppose

           A5: (f . n) < k;



           A6: ( min* (f " {k})) <= ((n + 1) - 1) by Th16;



           A7: ( rng f) = (k + 1) by A1, FUNCT_2:def 3;

          k < (k + 1) by NAT_1: 13;

          then k in ( rng f) by A7, NAT_1: 44;

          then ( min* (f " {(f . n)})) < ( min* (f " {k})) & k in NAT & n in NAT by A1, A5, A7, ORDINAL1:def 12;

          hence contradiction by A2, A6, Th5;

        end;

      end;

      hence contradiction;

    end;

    theorem :: STIRL2_1:35



     Th35: for f be Function of ( Segm (n + 1)), ( Segm k) st k <> 0 & (f " {(f . n)}) <> {n} holds ex m st m in (f " {(f . n)}) & m <> n

    proof

      let f be Function of ( Segm (n + 1)), ( Segm k) such that

       A1: k <> 0 and

       A2: (f " {(f . n)}) <> {n};



       A3: n < (n + 1) by NAT_1: 13;



       A4: (f . n) in {(f . n)} by TARSKI:def 1;

      ( dom f) = (n + 1) by A1, FUNCT_2:def 1;

      then n in ( dom f) by A3, NAT_1: 44;

      then n in (f " {(f . n)}) by A4, FUNCT_1:def 7;

      then ex m be object st m in (f " {(f . n)}) & m <> n by A2, ZFMISC_1: 35;

      hence thesis;

    end;

    theorem :: STIRL2_1:36



     Th36: for f be Function of ( Segm n), ( Segm k), g be Function of ( Segm (n + m)), ( Segm (k + l)) st g is "increasing & f = (g | n) holds for i, j st i in ( rng f) & j in ( rng f) & i < j holds ( min* (f " {i})) < ( min* (f " {j}))

    proof

      let f be Function of ( Segm n), ( Segm k), g be Function of ( Segm (n + m)), ( Segm (k + l)) such that

       A1: g is "increasing and

       A2: f = (g | n);

      let i, j such that

       A3: i in ( rng f) and

       A4: j in ( rng f) and

       A5: i < j;



       A6: for k1 be Element of NAT st k1 in ( rng f) holds k1 in ( rng g) & ( min* (f " {k1})) = ( min* (g " {k1}))

      proof



         A7: n is Subset of NAT by Th8;

        let k1 be Element of NAT such that

         A8: k1 in ( rng f);

        consider x be object such that

         A9: x in ( dom f) and

         A10: (f . x) = k1 by A8, FUNCT_1:def 3;



         A11: ( dom f) = n by A8, FUNCT_2:def 1;

        x in n by A9;

        then

        reconsider x9 = x as Element of NAT by A7;



         A12: x9 < n by A9, NAT_1: 44;



         A13: (f . x9) = (g . x9) by A2, A9, FUNCT_1: 47;

        ( Segm k) is non empty by A8;

        then k is non zero;

        then (k + l) is non zero;

        then ( Segm (k + l)) is non empty;

        then

         A14: ( dom g) = ( Segm (n + m)) by FUNCT_2:def 1;

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

        then

         A15: ( Segm n) c= ( Segm (n + m)) by NAT_1: 39;

         A16:

        now

          let n1 be Nat such that

           A17: n1 in (f " {k1});



           A18: n1 in n by A11, A17, FUNCT_1:def 7;

          (f . n1) in {k1} by A17, FUNCT_1:def 7;

          then (g . n1) in {k1} by A2, A11, A18, FUNCT_1: 47;

          then n1 in (g " {k1}) by A14, A15, A18, FUNCT_1:def 7;

          hence ( min* (g " {k1})) <= n1 by NAT_1:def 1;

        end;

        k1 in {k1} by TARSKI:def 1;

        then

         A19: x9 in (g " {k1}) by A9, A10, A11, A14, A15, A13, FUNCT_1:def 7;

        then ( min* (g " {k1})) <= x9 by NAT_1:def 1;

        then ( min* (g " {k1})) < n by A12, XXREAL_0: 2;

        then

         A20: ( min* (g " {k1})) in ( dom f) by A11, NAT_1: 44;

        ( min* (g " {k1})) in (g " {k1}) by A19, NAT_1:def 1;

        then (g . ( min* (g " {k1}))) in {k1} by FUNCT_1:def 7;

        then (f . ( min* (g " {k1}))) in {k1} by A2, A20, FUNCT_1: 47;

        then ( min* (g " {k1})) in (f " {k1}) by A20, FUNCT_1:def 7;

        hence thesis by A9, A10, A11, A14, A15, A13, A16, FUNCT_1:def 3, NAT_1:def 1;

      end;



       A21: i in NAT & j in NAT by ORDINAL1:def 12;

      then

       A22: j in ( rng g) by A4, A6;



       A23: ( min* (f " {j})) = ( min* (g " {j})) by A4, A6, A21;



       A24: ( min* (f " {i})) = ( min* (g " {i})) by A3, A6, A21;

      i in ( rng g) by A3, A6, A21;

      hence thesis by A1, A5, A22, A24, A23;

    end;

    theorem :: STIRL2_1:37



     Th37: for f be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f is onto "increasing & (f " {(f . n)}) = {n} holds ( rng (f | n)) c= ( Segm k) & for g be Function of ( Segm n), ( Segm k) st g = (f | n) holds g is onto "increasing

    proof

      let f be Function of ( Segm (n + 1)), ( Segm (k + 1)) such that

       A1: f is onto "increasing and

       A2: (f " {(f . n)}) = {n};

      now

        per cases ;

          suppose

           A3: n = 0 ;

          then ( 0 + 1) >= (k + 1) by A1, Th17;

          then k = 0 by XREAL_1: 6;

          hence thesis by A3, Th15;

        end;

          suppose

           A4: n > 0 ;

          thus

           A5: ( rng (f | n)) c= ( Segm k)

          proof

            let fi be object such that

             A6: fi in ( rng (f | n));

            ( rng (f | n)) c= ( rng f) by RELAT_1: 70;

            then fi in ( rng f) by A6;

            then

             A7: fi in (k + 1);

            (k + 1) is Subset of NAT by Th8;

            then

            reconsider fi as Element of NAT by A7;

            consider i be object such that

             A8: i in ( dom (f | n)) and

             A9: ((f | n) . i) = fi by A6, FUNCT_1:def 3;

            i in (( dom f) /\ n) by A8, RELAT_1: 61;

            then

             A10: i in n by XBOOLE_0:def 4;

            n is Subset of NAT by Th8;

            then

            reconsider i as Element of NAT by A10;



             A11: (f . i) < k

            proof

              (f . i) < (k + 1) by NAT_1: 44;

              then

               A12: (f . i) <= k by NAT_1: 13;

              assume (f . i) >= k;

              then

               A13: (f . i) = k by A12, XXREAL_0: 1;



               A14: (f . i) in {(f . i)} by TARSKI:def 1;



               A15: (f . n) = k by A1, A2, Th34;



               A16: i in (( dom f) /\ n) by A8, RELAT_1: 61;

              then i in ( dom f) by XBOOLE_0:def 4;

              then i in (f " {(f . n)}) by A13, A14, A15, FUNCT_1:def 7;

              then i >= ( min* (f " {(f . n)})) & i in NAT & n in NAT by NAT_1:def 1, ORDINAL1:def 12;

              then

               A17: i >= n by A2, Th5;

              i in ( Segm n) by A16, XBOOLE_0:def 4;

              hence contradiction by A17, NAT_1: 44;

            end;

            (f . i) = ((f | n) . i) by A8, FUNCT_1: 47;

            hence thesis by A9, A11, NAT_1: 44;

          end;

          thus for g be Function of ( Segm n), ( Segm k) st g = (f | n) holds g is onto "increasing

          proof

            let g be Function of ( Segm n), ( Segm k) such that

             A18: g = (f | n);

            ( Segm k) c= ( rng g)

            proof

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

              then

               A19: ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;

              ( dom f) = (n + 1) by FUNCT_2:def 1;

              then

               A20: n = (( dom f) /\ n) by A19, XBOOLE_1: 28;

              let k1 be object such that

               A21: k1 in ( Segm k);

              reconsider k9 = k1 as Element of NAT by A21;

              k9 < k by A21, NAT_1: 44;

              then k9 < (k + 1) by NAT_1: 13;

              then

               A22: k9 in ( Segm (k + 1)) by NAT_1: 44;



               A23: ( dom f) = (n + 1) by FUNCT_2:def 1;

              ( rng f) = (k + 1) by A1, FUNCT_2:def 3;

              then

              consider n1 be object such that

               A24: n1 in ( dom f) and

               A25: (f . n1) = k9 by A22, FUNCT_1:def 3;

              reconsider n1 as Element of NAT by A24, A23;

              n1 < (n + 1) by A24, NAT_1: 44;

              then

               A26: n1 <= n by NAT_1: 13;

              reconsider nn = k1 as set by TARSKI: 1;



               A: not nn in nn;

              (f . n) = k by A1, A2, Th34;

              then n1 <> n by A, A21, A25;

              then

               A27: n1 < n by A26, XXREAL_0: 1;

              (( dom f) /\ n) = ( dom (f | n)) by RELAT_1: 61;

              then

               A28: n1 in ( dom g) by A18, A27, A20, NAT_1: 44;

              then (g . n1) in ( rng g) by FUNCT_1:def 3;

              hence thesis by A18, A25, A28, FUNCT_1: 47;

            end;

            then k = ( rng g);

            hence g is onto by FUNCT_2:def 3;



             A29: (( dom f) /\ n) = ( dom (f | n)) by RELAT_1: 61;

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

            then

             A30: ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;

            ( dom f) = (n + 1) by FUNCT_2:def 1;

            then

             A31: n = (( dom f) /\ n) by A30, XBOOLE_1: 28;

             0 in ( Segm n) by A4, NAT_1: 44;

            then ((f | n) . 0 ) in ( rng (f | n)) by A31, A29, FUNCT_1:def 3;

            then

             A32: n = 0 iff k = 0 by A5;

            for i, j st i in ( rng g) & j in ( rng g) & i < j holds ( min* (g " {i})) < ( min* (g " {j})) by A1, A18, Th36;

            hence g is "increasing by A32;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:38



     Th38: for f be Function of ( Segm (n + 1)), ( Segm k), g be Function of ( Segm n), ( Segm k) st f is onto "increasing & (f " {(f . n)}) <> {n} & (f | n) = g holds g is onto "increasing

    proof

      let f be Function of ( Segm (n + 1)), ( Segm k), g be Function of ( Segm n), ( Segm k) such that

       A1: f is onto "increasing and

       A2: (f " {(f . n)}) <> {n} and

       A3: (f | n) = g;

      now

        per cases ;

          suppose k = 0 ;

          hence thesis by A1;

        end;

          suppose

           A4: k > 0 ;



           A5: ( rng f) = k by A1, FUNCT_2:def 3;

          now

            k = (k + 0 );

            then

             A6: for i, j st i in ( rng g) & j in ( rng g) & i < j holds ( min* (g " {i})) < ( min* (g " {j})) by A1, A3, Th36;



             A7: k c= ( rng g)

            proof

              let k1 be object such that

               A8: k1 in k;

              consider x be object such that

               A9: x in ( dom f) and

               A10: (f . x) = k1 by A5, A8, FUNCT_1:def 3;

              ( dom f) = (n + 1) by A8, FUNCT_2:def 1;

              then

              reconsider x as Element of NAT by A9;

              x < (n + 1) by A9, NAT_1: 44;

              then

               A11: x <= n by NAT_1: 13;

              now

                per cases by A11, XXREAL_0: 1;

                  suppose

                   A12: x < n;



                   A13: ( dom g) = n by A4, FUNCT_2:def 1;



                   A14: x in ( Segm n) by A12, NAT_1: 44;

                  then (g . x) = (f . x) by A3, A13, FUNCT_1: 47;

                  hence thesis by A10, A14, A13, FUNCT_1:def 3;

                end;

                  suppose x = n;

                  then

                  consider m such that

                   A15: m in (f " {k1}) and

                   A16: m <> n by A2, A4, A10, Th35;

                  (f . m) in {k1} by A15, FUNCT_1:def 7;

                  then

                   A17: (f . m) = k1 by TARSKI:def 1;

                  m in ( dom f) by A15, FUNCT_1:def 7;

                  then m < (n + 1) by NAT_1: 44;

                  then m <= n by NAT_1: 13;

                  then m < n by A16, XXREAL_0: 1;

                  then

                   A18: m in ( Segm n) by NAT_1: 44;



                   A19: n = ( dom g) by A4, FUNCT_2:def 1;

                  then (g . m) = (f . m) by A3, A18, FUNCT_1: 47;

                  hence thesis by A18, A19, A17, FUNCT_1:def 3;

                end;

              end;

              hence thesis;

            end;

            then

             A20: ( rng g) = k;

            n = 0 iff k = 0 by A4, A7;

            hence thesis by A20, A6, FUNCT_2:def 3;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:39



     Th39: for f be Function of ( Segm n), ( Segm k), g be Function of ( Segm (n + 1)), ( Segm (k + m)) st f is onto "increasing & f = (g | n) holds for i, j st i in ( rng g) & j in ( rng g) & i < j holds ( min* (g " {i})) < ( min* (g " {j}))

    proof

      let f be Function of ( Segm n), ( Segm k), g be Function of ( Segm (n + 1)), ( Segm (k + m)) such that

       A1: f is onto "increasing and

       A2: f = (g | n);



       A3: for i st i < n holds (f . i) = (g . i)

      proof

        k = 0 iff n = 0 by A1;

        then

         A4: ( dom f) = n by FUNCT_2:def 1;

        let i;

        assume i < n;

        then i in ( Segm n) by NAT_1: 44;

        hence thesis by A2, A4, FUNCT_1: 47;

      end;



       A5: for l st l in ( rng g) & not l in ( rng f) holds l = (g . n)

      proof

        let l such that

         A6: l in ( rng g) and

         A7: not l in ( rng f);

        consider x be object such that

         A8: x in ( dom g) and

         A9: (g . x) = l by A6, FUNCT_1:def 3;

        assume

         A10: l <> (g . n);

        ( dom g) = (n + 1) by A6, FUNCT_2:def 1;

        then

        reconsider x as Element of NAT by A8;

        x < (n + 1) by A8, NAT_1: 44;

        then x <= n by NAT_1: 13;

        then

         A11: x < n by A10, A9, XXREAL_0: 1;

        then

         A12: x in ( Segm n) by NAT_1: 44;

        k <> 0 by A1, A11;

        then

         A13: ( dom f) = n by FUNCT_2:def 1;

        (f . x) = (g . x) by A3, A11;

        hence contradiction by A7, A9, A13, A12, FUNCT_1:def 3;

      end;



       A14: for l st l in ( rng g) & not l in ( rng f) holds ( min* (g " {l})) = n

      proof



         A15: n < (n + 1) by NAT_1: 13;

        let l such that

         A16: l in ( rng g) and

         A17: not l in ( rng f);



         A18: l in {l} by TARSKI:def 1;

        ( dom g) = (n + 1) by A16, FUNCT_2:def 1;

        then

         A19: n in ( dom g) by A15, NAT_1: 44;

        (g . n) = l by A5, A16, A17;

        then n in (g " {l}) by A19, A18, FUNCT_1:def 7;

        then ( min* (g " {l})) in (g " {l}) by NAT_1:def 1;

        then

         A20: (g . ( min* (g " {l}))) in {l} by FUNCT_1:def 7;

        assume

         A21: ( min* (g " {l})) <> n;

        ( min* (g " {l})) <= ((n + 1) - 1) by Th16;

        then

         A22: ( min* (g " {l})) < n by A21, XXREAL_0: 1;

        then k <> 0 by A1;

        then

         A23: ( dom f) = n by FUNCT_2:def 1;

        ( min* (g " {l})) in ( Segm n) by A22, NAT_1: 44;

        then

         A24: (f . ( min* (g " {l}))) in ( rng f) by A23, FUNCT_1:def 3;

        (f . ( min* (g " {l}))) = (g . ( min* (g " {l}))) by A3, A22;

        hence contradiction by A17, A20, A24, TARSKI:def 1;

      end;



       A25: for k1 be Element of NAT st k1 in ( rng f) holds ( min* (g " {k1})) = ( min* (f " {k1}))

      proof

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

        then

         A26: ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;

        let k1 be Element of NAT such that

         A27: k1 in ( rng f);

        consider x be object such that

         A28: x in ( dom f) and

         A29: (f . x) = k1 by A27, FUNCT_1:def 3;



         A30: x in n by A28;

        ( Segm k) is non empty by A27;

        then k is non zero;

        then (k + m) is non zero;

        then ( Segm (k + m)) is non empty;

        then

         A31: ( dom g) = ( Segm (n + 1)) by FUNCT_2:def 1;

        n is Subset of NAT by Th8;

        then

        reconsider x as Element of NAT by A30;

        k1 in {k1} by TARSKI:def 1;

        then

         A32: x in (f " {k1}) by A28, A29, FUNCT_1:def 7;

        then

         A33: ( min* (f " {k1})) <= x by NAT_1:def 1;



         A34: x < n by A28, NAT_1: 44;

        then

         A35: ( min* (f " {k1})) < n by A33, XXREAL_0: 2;



         A36: ( dom f) = n by A27, FUNCT_2:def 1;

         A37:

        now

          let n1 be Nat such that

           A38: n1 in (g " {k1});

          n1 in ( Segm (n + 1)) by A31, A38, FUNCT_1:def 7;

          then n1 < (n + 1) by NAT_1: 44;

          then

           A39: n1 <= n by NAT_1: 13;

          now

            per cases by A39, XXREAL_0: 1;

              suppose

               A40: n1 < n;

              (g . n1) in {k1} by A38, FUNCT_1:def 7;

              then

               A41: (f . n1) in {k1} by A3, A40;

              n1 in ( dom f) by A36, A40, NAT_1: 44;

              then n1 in (f " {k1}) by A41, FUNCT_1:def 7;

              hence ( min* (f " {k1})) <= n1 by NAT_1:def 1;

            end;

              suppose n1 = n;

              hence ( min* (f " {k1})) <= n1 by A33, A34, XXREAL_0: 2;

            end;

          end;

          hence ( min* (f " {k1})) <= n1;

        end;

        ( min* (f " {k1})) in (f " {k1}) by A32, NAT_1:def 1;

        then (f . ( min* (f " {k1}))) in {k1} by FUNCT_1:def 7;

        then

         A42: (g . ( min* (f " {k1}))) in {k1} by A3, A35;

        ( min* (f " {k1})) in n by A35, NAT_1: 44;

        then ( min* (f " {k1})) in (g " {k1}) by A31, A26, A42, FUNCT_1:def 7;

        hence thesis by A37, NAT_1:def 1;

      end;

      let i, j such that

       A43: i in ( rng g) and

       A44: j in ( rng g) and

       A45: i < j;



       A46: for l st l in ( rng g) & not l in ( rng f) holds l >= k

      proof

        let l such that l in ( rng g) and

         A47: not l in ( rng f);

        assume l < k;

        then l in ( Segm k) by NAT_1: 44;

        hence thesis by A1, A47, FUNCT_2:def 3;

      end;



       A48: i in NAT & j in NAT by ORDINAL1:def 12;

      now

        per cases ;

          suppose

           A49: i in ( rng f) & j in ( rng f);

          then

           A50: ( min* (g " {j})) = ( min* (f " {j})) by A25, A48;

          ( min* (g " {i})) = ( min* (f " {i})) by A25, A49, A48;

          hence thesis by A1, A45, A49, A50;

        end;

          suppose

           A51: i in ( rng f) & not j in ( rng f);

          then

           A52: n <> 0 ;

          then ( min* (f " {i})) <= (n - 1) by Th16;

          then

           A53: ( min* (g " {i})) <= (n - 1) by A25, A51, A48;

          (n - 1) is Element of NAT by A52, NAT_1: 20;

          then

           A54: (n - 1) < ((n - 1) + 1) by NAT_1: 13;

          ( min* (g " {j})) = n by A44, A14, A51;

          hence thesis by A53, A54, XXREAL_0: 2;

        end;

          suppose

           A55: not i in ( rng f) & j in ( rng f);

          then

           A56: j < k by NAT_1: 44;

          i >= k by A43, A46, A55;

          hence thesis by A45, A56, XXREAL_0: 2;

        end;

          suppose

           A57: not i in ( rng f) & not j in ( rng f);

          then i = (g . n) by A43, A5;

          hence thesis by A44, A45, A5, A57;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:40



     Th40: for f be Function of ( Segm n), ( Segm k), g be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f is onto "increasing & f = (g | ( Segm n)) & (g . n) = k holds g is onto "increasing & (g " {(g . n)}) = {n}

    proof

      let f be Function of ( Segm n), ( Segm k), g be Function of ( Segm (n + 1)), ( Segm (k + 1)) such that

       A1: f is onto "increasing and

       A2: f = (g | ( Segm n)) and

       A3: (g . n) = k;

      ( Segm (k + 1)) c= ( rng g)

      proof

        let x9 be object such that

         A4: x9 in ( Segm (k + 1));

        reconsider x = x9 as Element of NAT by A4;

        x < (k + 1) by A4, NAT_1: 44;

        then

         A5: x <= k by NAT_1: 13;

        now

          per cases by A5, XXREAL_0: 1;

            suppose

             A6: x < k;



             A7: ( rng f) = k by A1, FUNCT_2:def 3;

            x in ( Segm k) by A6, NAT_1: 44;

            then

            consider y be object such that

             A8: y in ( dom f) and

             A9: (f . y) = x by A7, FUNCT_1:def 3;



             A10: ( dom g) = (n + 1) by FUNCT_2:def 1;

            n = 0 iff k = 0 by A1;

            then

             A11: ( dom f) = n by FUNCT_2:def 1;

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

            then

             A12: ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;

            (f . y) = (g . y) by A2, A8, FUNCT_1: 47;

            hence thesis by A8, A9, A11, A12, A10, FUNCT_1:def 3;

          end;

            suppose

             A13: x = k;

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

            then

             A14: n in ( Segm (n + 1)) by NAT_1: 44;

            ( dom g) = (n + 1) by FUNCT_2:def 1;

            hence thesis by A3, A13, A14, FUNCT_1:def 3;

          end;

        end;

        hence thesis;

      end;

      then (k + 1) = ( rng g);

      hence g is onto by FUNCT_2:def 3;

      for i, j st i in ( rng g) & j in ( rng g) & i < j holds ( min* (g " {i})) < ( min* (g " {j})) by A1, A2, Th39;

      hence g is "increasing;

      thus (g " {(g . n)}) = {n}

      proof

        assume (g " {(g . n)}) <> {n};

        then

        consider m such that

         A15: m in (g " {(g . n)}) and

         A16: m <> n by Th35;

        (g . m) in {(g . n)} by A15, FUNCT_1:def 7;

        then

         A17: (g . m) = k by A3, TARSKI:def 1;

        m in ( dom g) by A15, FUNCT_1:def 7;

        then m < (n + 1) by NAT_1: 44;

        then m <= n by NAT_1: 13;

        then

         A18: m < n by A16, XXREAL_0: 1;

        n = 0 iff k = 0 by A1;

        then ( dom f) = n by FUNCT_2:def 1;

        then

         A19: m in ( dom f) by A18, NAT_1: 44;

        then

         A20: (f . m) in ( rng f) by FUNCT_1:def 3;

        (f . m) = (g . m) by A2, A19, FUNCT_1: 47;

        hence contradiction by A20, A17, NAT_1: 44;

      end;

    end;

    theorem :: STIRL2_1:41



     Th41: for f be Function of ( Segm n), ( Segm k), g be Function of ( Segm (n + 1)), ( Segm k) st f is onto "increasing & f = (g | ( Segm n)) & (g . n) < k holds g is onto "increasing & (g " {(g . n)}) <> {n}

    proof

      let f be Function of ( Segm n), ( Segm k), g be Function of ( Segm (n + 1)), ( Segm k) such that

       A1: f is onto "increasing and

       A2: f = (g | ( Segm n)) and

       A3: (g . n) < k;

      k = ( rng f) by A1, FUNCT_2:def 3;

      then

      consider x be object such that

       A4: x in ( dom f) and

       A5: (f . x) = (g . n) by A3, FUNCT_1:def 3;

      (g . n) = (g . x) by A2, A4, A5, FUNCT_1: 47;

      then

       A6: (g . x) in {(g . n)} by TARSKI:def 1;

      k c= ( rng g)

      proof

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

        then

         A7: ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;

        n = 0 iff k = 0 by A1;

        then

         A8: ( dom f) = n by FUNCT_2:def 1;

        let x9 be object such that

         A9: x9 in k;

        k is Subset of NAT by Th8;

        then

        reconsider x = x9 as Element of NAT by A9;

        ( rng f) = k by A1, FUNCT_2:def 3;

        then

        consider y be object such that

         A10: y in ( dom f) and

         A11: (f . y) = x by A9, FUNCT_1:def 3;



         A12: ( dom g) = (n + 1) by A3, FUNCT_2:def 1;

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

        hence thesis by A10, A11, A8, A7, A12, FUNCT_1:def 3;

      end;

      then k = ( rng g);

      hence g is onto by FUNCT_2:def 3;

      k = (k + 0 );

      then for i, j st i in ( rng g) & j in ( rng g) & i < j holds ( min* (g " {i})) < ( min* (g " {j})) by A1, A2, Th39;

      hence g is "increasing by A3;

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

      then

       A13: ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;

      reconsider nn = n as set;



       A: not nn in nn;



       A14: x in n by A4;

      then

       A15: x <> n by A;

      ( dom g) = (n + 1) by A3, FUNCT_2:def 1;

      then x in (g " {(g . n)}) by A14, A13, A6, FUNCT_1:def 7;

      hence thesis by A15, TARSKI:def 1;

    end;



     Lm1: k < n implies (n \/ {k}) = n

    proof

      assume k < n;

      then k in ( Segm n) by NAT_1: 44;

      then {k} c= n by ZFMISC_1: 31;

      hence thesis by XBOOLE_1: 12;

    end;

    theorem :: STIRL2_1:42



     Th42: ( card { f where f be Function of ( Segm (n + 1)), ( Segm (k + 1)) : f is onto "increasing & (f " {(f . n)}) = {n} }) = ( card { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing })

    proof

      set F1 = { f where f be Function of ( Segm (n + 1)), ( Segm (k + 1)) : f is onto "increasing & (f " {(f . n)}) = {n} };

      set F2 = { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing };

      now

        per cases ;

          suppose

           A1: k = 0 & n <> 0 ;



           A2: F1 is empty

          proof

            assume F1 is non empty;

            then

            consider x be object such that

             A3: x in F1;

            consider f be Function of ( Segm (n + 1)), ( Segm (k + 1)) such that x = f and f is onto "increasing and

             A4: (f " {(f . n)}) = {n} by A3;

             0 in ( Segm (n + 1)) by NAT_1: 44;

            then

             A5: 0 in ( dom f) by FUNCT_2:def 1;



             A6: 0 in { 0 } by TARSKI:def 1;



             A7: (f . 0 ) = 0 by A1, CARD_1: 49, TARSKI:def 1;

            (f . n) = 0 by A1, CARD_1: 49, TARSKI:def 1;

            then 0 in {n} by A4, A7, A5, A6, FUNCT_1:def 7;

            hence thesis by A1;

          end;

          (n block k) = 0 by A1, Th31;

          hence thesis by A2;

        end;

          suppose

           A8: k = 0 implies n = 0 ;

          defpred P[ object, set, set] means for i, j st ( Segm i) = $2 & ( Segm j) = $3 holds ex f be Function of ( Segm i), ( Segm j) st f = $1 & f is onto "increasing & (n < i implies (f " {(f . n)}) = {n});



           A9: not n in ( Segm n);

          set FF2 = { f where f be Function of ( Segm n), ( Segm k) : P[f, ( Segm n), ( Segm k)] };

          set FF1 = { f where f be Function of (( Segm n) \/ {n}), (( Segm k) \/ {k}) : P[f, (( Segm n) \/ {n}), (( Segm k) \/ {k})] & ( rng (f | ( Segm n))) c= ( Segm k) & (f . n) = k };



           A10: for f be Function of (( Segm n) \/ {n}), (( Segm k) \/ {k}) st (f . n) = k holds P[f, (( Segm n) \/ {n}), (( Segm k) \/ {k})] iff P[(f | ( Segm n)), ( Segm n), ( Segm k)]

          proof

            let f9 be Function of (( Segm n) \/ {n}), (( Segm k) \/ {k}) such that

             A11: (f9 . n) = k;

            thus P[f9, (( Segm n) \/ {n}), (( Segm k) \/ {k})] implies P[(f9 | ( Segm n)), ( Segm n), ( Segm k)]

            proof

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

              then

               A12: ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;



               A13: ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;



               A14: ( Segm (k + 1)) = (( Segm k) \/ {k}) by AFINSQ_1: 2;

              assume P[f9, (( Segm n) \/ {n}), (( Segm k) \/ {k})];

              then

              consider f be Function of ( Segm (n + 1)), ( Segm (k + 1)) such that

               A15: f = f9 and

               A16: f is onto "increasing and

               A17: n < (n + 1) implies (f " {(f . n)}) = {n} by A13, A14;



               A18: ( rng (f | n)) c= ( Segm k) by A16, A17, Th37, NAT_1: 13;



               A19: ( dom (f | n)) = (( dom f) /\ n) by RELAT_1: 61;

              ( dom f) = (n + 1) by FUNCT_2:def 1;

              then ( dom (f | n)) = n by A12, A19, XBOOLE_1: 28;

              then

              reconsider fn = (f | n) as Function of n, k by A18, FUNCT_2: 2;

              let i, j such that

               A20: ( Segm i) = ( Segm n) and

               A21: ( Segm j) = ( Segm k);

              reconsider fi = fn as Function of ( Segm i), ( Segm j) by A20, A21;

              fi is onto "increasing by A16, A17, A20, A21, Th37, NAT_1: 13;

              hence thesis by A15, A20;

            end;

            thus P[(f9 | ( Segm n)), ( Segm n), ( Segm k)] implies P[f9, (( Segm n) \/ {n}), (( Segm k) \/ {k})]

            proof

              (( Segm n) \/ {n}) = ( Segm (n + 1)) by AFINSQ_1: 2;

              then

              reconsider f = f9 as Function of ( Segm (n + 1)), ( Segm (k + 1)) by AFINSQ_1: 2;

              assume P[(f9 | ( Segm n)), ( Segm n), ( Segm k)];

              then

               A22: ex fn be Function of ( Segm n), ( Segm k) st fn = (f9 | n) & fn is onto "increasing & (n < n implies (fn " {(fn . n)}) = {n});

              let i, j such that

               A23: ( Segm i) = (( Segm n) \/ {n}) and

               A24: ( Segm j) = (( Segm k) \/ {k});

              reconsider f1 = f as Function of ( Segm i), ( Segm j) by A23, A24;



               A25: for f be Function of ( Segm n), ( Segm k), f1 be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f is onto "increasing & f = (f1 | ( Segm n)) & (f1 . n) = k holds (f1 " {(f1 . n)}) = {n} by Th40;



               A26: n < i implies (f1 " {(f1 . n)}) = {n} by A11, A22, A25;



               A27: ( Segm (k + 1)) = j by A24, AFINSQ_1: 2;

              ( Segm (n + 1)) = i by A23, AFINSQ_1: 2;

              then f1 is onto "increasing by A11, A22, A27, Th40;

              hence thesis by A26;

            end;

          end;



           A28: ( Segm k) is empty implies ( Segm n) is empty by A8;



           A29: ( card FF2) = ( card FF1) from Sch4( A28, A9, A10);



           A30: F2 c= FF2

          proof

            let x be object;

            assume x in F2;

            then

             A31: ex f be Function of ( Segm n), ( Segm k) st x = f & f is onto "increasing;

            then P[x, n, k];

            hence thesis by A31;

          end;



           A32: F1 c= FF1

          proof

            let x be object;

            assume x in F1;

            then

            consider f be Function of ( Segm (n + 1)), ( Segm (k + 1)) such that

             A33: f = x and

             A34: f is onto "increasing and

             A35: (f " {(f . n)}) = {n};



             A36: ( rng (f | n)) c= ( Segm k) by A34, A35, Th37;



             A37: P[f, (( Segm n) \/ {n}), (( Segm k) \/ {k})]

            proof

              let i, j such that

               A38: ( Segm i) = (( Segm n) \/ {n}) and

               A39: ( Segm j) = (( Segm k) \/ {k});



               A40: ( Segm j) = ( Segm (k + 1)) by A39, AFINSQ_1: 2;

              ( Segm i) = ( Segm (n + 1)) by A38, AFINSQ_1: 2;

              hence thesis by A34, A35, A40;

            end;



             A41: ( Segm (k + 1)) = (( Segm k) \/ {k}) by AFINSQ_1: 2;



             A42: ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;

            (f . n) = k by A34, A35, Th34;

            hence thesis by A33, A37, A36, A42, A41;

          end;



           A43: FF2 c= F2

          proof

            let x be object;

            assume x in FF2;

            then

            consider f be Function of n, k such that

             A44: x = f and

             A45: P[f, n, k];

            ex g be Function of ( Segm n), ( Segm k) st g = f & g is onto "increasing & (n < n implies (g " {(g . n)}) = {n}) by A45;

            hence thesis by A44;

          end;

          FF1 c= F1

          proof

            let x be object;

            assume x in FF1;

            then

            consider f be Function of (n \/ {n}), (k \/ {k}) such that

             A46: x = f and

             A47: P[f, (n \/ {n}), (k \/ {k})] and ( rng (f | n)) c= k and (f . n) = k;



             A48: ( Segm (k + 1)) = (( Segm k) \/ {k}) by AFINSQ_1: 2;

            ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;

            then ex f9 be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f = f9 & f9 is onto "increasing & (n < (n + 1) implies (f9 " {(f9 . n)}) = {n}) by A47, A48;

            hence thesis by A46, NAT_1: 13;

          end;

          then F1 = FF1 by A32;

          hence thesis by A29, A30, A43, XBOOLE_0:def 10;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:43



     Th43: for l st l < k holds ( card { f where f be Function of ( Segm (n + 1)), ( Segm k) : f is onto "increasing & (f " {(f . n)}) <> {n} & (f . n) = l }) = ( card { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing })

    proof

      let l such that

       A1: l < k;

      set F2 = { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing };

      set F1 = { f where f be Function of ( Segm (n + 1)), ( Segm k) : f is onto "increasing & (f " {(f . n)}) <> {n} & (f . n) = l };

      now

        per cases ;

          suppose k = 0 & n <> 0 ;

          hence thesis by A1;

        end;

          suppose

           A2: k = 0 implies n = 0 ;

          defpred P[ object, set, set] means for i, j st ( Segm i) = $2 & ( Segm j) = $3 holds ex f be Function of ( Segm i), ( Segm j) st f = $1 & f is onto "increasing & (n < i implies (f " {(f . n)}) <> {n});



           A3: not n in ( Segm n);

          set FF2 = { f where f be Function of ( Segm n), ( Segm k) : P[f, ( Segm n), ( Segm k)] };

          set FF1 = { f where f be Function of (( Segm n) \/ {n}), (( Segm k) \/ {l}) : P[f, (( Segm n) \/ {n}), (( Segm k) \/ {l})] & ( rng (f | ( Segm n))) c= ( Segm k) & (f . n) = l };



           A4: for f be Function of (( Segm n) \/ {n}), (( Segm k) \/ {l}) st (f . n) = l holds P[f, (( Segm n) \/ {n}), (( Segm k) \/ {l})] iff P[(f | ( Segm n)), ( Segm n), ( Segm k)]

          proof

            let f9 be Function of (( Segm n) \/ {n}), (( Segm k) \/ {l}) such that

             A5: (f9 . n) = l;

            thus P[f9, (( Segm n) \/ {n}), (( Segm k) \/ {l})] implies P[(f9 | ( Segm n)), ( Segm n), ( Segm k)]

            proof

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

              then

               A6: ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;

              assume

               A7: P[f9, (( Segm n) \/ {n}), (( Segm k) \/ {l})];



               A8: ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;

              k = (k \/ {l}) by A1, Lm1;

              then

              consider f be Function of ( Segm (n + 1)), ( Segm k) such that

               A9: f = f9 and

               A10: f is onto "increasing and

               A11: n < (n + 1) implies (f " {(f . n)}) <> {n} by A7, A8;



               A12: ( dom (f | n)) = (( dom f) /\ n) by RELAT_1: 61;

              ( rng (f | n)) c= ( rng f) by RELAT_1: 70;

              then

               A13: ( rng (f | n)) c= ( Segm k) by XBOOLE_1: 1;

              ( dom f) = (n + 1) by A1, FUNCT_2:def 1;

              then ( dom (f | n)) = n by A6, A12, XBOOLE_1: 28;

              then

              reconsider fn = (f | n) as Function of ( Segm n), ( Segm k) by A13, FUNCT_2: 2;

              let i, j such that

               A14: ( Segm i) = ( Segm n) and

               A15: ( Segm j) = ( Segm k);

              reconsider fi = fn as Function of ( Segm i), ( Segm j) by A14, A15;

              fi is onto "increasing by A10, A11, A14, A15, Th38, NAT_1: 13;

              hence thesis by A9, A14;

            end;

            thus P[(f9 | ( Segm n)), ( Segm n), ( Segm k)] implies P[f9, (( Segm n) \/ {n}), (( Segm k) \/ {l})]

            proof

              (( Segm n) \/ {n}) = ( Segm (n + 1)) by AFINSQ_1: 2;

              then

              reconsider f = f9 as Function of (n + 1), k by A1, Lm1;

              assume P[(f9 | ( Segm n)), ( Segm n), ( Segm k)];

              then

               A16: ex fn be Function of ( Segm n), ( Segm k) st fn = (f9 | n) & fn is onto "increasing & (n < n implies (fn " {(fn . n)}) <> {n});

              let i, j such that

               A17: ( Segm i) = (( Segm n) \/ {n}) and

               A18: ( Segm j) = (( Segm k) \/ {l});

              reconsider f1 = f as Function of ( Segm i), ( Segm j) by A17, A18;

              for f be Function of ( Segm n), ( Segm k), g be Function of ( Segm (n + 1)), ( Segm k) st f is onto "increasing & f = (g | ( Segm n)) & (g . n) < k holds g is onto "increasing & (g " {(g . n)}) <> {n} by Th41;

              then

               A19: n < i implies (f1 " {(f1 . n)}) <> {n} by A1, A5, A16;



               A20: ( Segm (n + 1)) = i by A17, AFINSQ_1: 2;

              k = j by A1, A18, Lm1;

              then f1 is onto "increasing by A1, A5, A16, A20, Th41;

              hence thesis by A19;

            end;

          end;



           A21: ( Segm k) is empty implies ( Segm n) is empty by A2;



           A22: ( card FF2) = ( card FF1) from Sch4( A21, A3, A4);



           A23: F2 c= FF2

          proof

            let x be object;

            assume x in F2;

            then

             A24: ex f be Function of ( Segm n), ( Segm k) st x = f & f is onto "increasing;

            then P[x, n, k];

            hence thesis by A24;

          end;



           A25: F1 c= FF1

          proof

            let x be object;

            assume x in F1;

            then

            consider f be Function of ( Segm (n + 1)), ( Segm k) such that

             A26: f = x and

             A27: f is onto "increasing and

             A28: (f " {(f . n)}) <> {n} and

             A29: (f . n) = l;



             A30: P[f, (( Segm n) \/ {n}), (( Segm k) \/ {l})]

            proof

              let i, j such that

               A31: ( Segm i) = (( Segm n) \/ {n}) and

               A32: ( Segm j) = (( Segm k) \/ {l});



               A33: i = ( Segm (n + 1)) by A31, AFINSQ_1: 2;

              j = k by A1, A32, Lm1;

              hence thesis by A27, A28, A33;

            end;



             A34: k = (k \/ {l}) by A1, Lm1;



             A35: ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;

            ( rng (f | ( Segm n))) c= ( rng f) by RELAT_1: 70;

            then ( rng (f | ( Segm n))) c= ( Segm k) by XBOOLE_1: 1;

            hence thesis by A26, A29, A30, A35, A34;

          end;



           A36: FF2 c= F2

          proof

            let x be object;

            assume x in FF2;

            then

            consider f be Function of n, k such that

             A37: x = f and

             A38: P[f, n, k];

            ex g be Function of ( Segm n), ( Segm k) st g = f & g is onto "increasing & (n < n implies (g " {(g . n)}) <> {n}) by A38;

            hence thesis by A37;

          end;

          FF1 c= F1

          proof



             A39: ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;

            let x be object;

            assume x in FF1;

            then

            consider f be Function of (n \/ {n}), (k \/ {l}) such that

             A40: x = f and

             A41: P[f, (n \/ {n}), (k \/ {l})] and ( rng (f | n)) c= k and

             A42: (f . n) = l;

            k = (k \/ {l}) by A1, Lm1;

            then ex f9 be Function of ( Segm (n + 1)), ( Segm k) st f = f9 & f9 is onto "increasing & (n < (n + 1) implies (f9 " {(f9 . n)}) <> {n}) by A41, A39;

            hence thesis by A40, A42, NAT_1: 13;

          end;

          then F1 = FF1 by A25;

          hence thesis by A22, A23, A36, XBOOLE_0:def 10;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:44



     Th44: for f be Function, n holds (( union ( rng (f | n))) \/ (f . n)) = ( union ( rng (f | (n + 1))))

    proof

      let f be Function, n;

      thus (( union ( rng (f | n))) \/ (f . n)) c= ( union ( rng (f | (n + 1))))

      proof

        let x be object such that

         A1: x in (( union ( rng (f | n))) \/ (f . n));

        now

          per cases by A1, XBOOLE_0:def 3;

            suppose x in ( union ( rng (f | n)));

            then

            consider Y be set such that

             A2: x in Y and

             A3: Y in ( rng (f | n)) by TARSKI:def 4;

            consider X be object such that

             A4: X in ( dom (f | n)) and

             A5: ((f | n) . X) = Y by A3, FUNCT_1:def 3;



             A6: ((f | n) . X) = (f . X) by A4, FUNCT_1: 47;

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

            then ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;

            then

             A7: (( dom f) /\ n) c= (( dom f) /\ (n + 1)) by XBOOLE_1: 26;

            X in (( dom f) /\ n) by A4, RELAT_1: 61;

            then X in (( dom f) /\ (n + 1)) by A7;

            then

             A8: X in ( dom (f | (n + 1))) by RELAT_1: 61;

            then

             A9: ((f | (n + 1)) . X) = (f . X) by FUNCT_1: 47;

            ((f | (n + 1)) . X) in ( rng (f | (n + 1))) by A8, FUNCT_1:def 3;

            hence thesis by A2, A5, A9, A6, TARSKI:def 4;

          end;

            suppose

             A10: x in (f . n);

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

            then

             A11: n in ( Segm (n + 1)) by NAT_1: 44;

            n in ( dom f) by A10, FUNCT_1:def 2;

            then n in (( dom f) /\ (n + 1)) by A11, XBOOLE_0:def 4;

            then

             A12: n in ( dom (f | (n + 1))) by RELAT_1: 61;

            then

             A13: ((f | (n + 1)) . n) = (f . n) by FUNCT_1: 47;

            ((f | (n + 1)) . n) in ( rng (f | (n + 1))) by A12, FUNCT_1:def 3;

            hence thesis by A10, A13, TARSKI:def 4;

          end;

        end;

        hence thesis;

      end;

      thus ( union ( rng (f | (n + 1)))) c= (( union ( rng (f | n))) \/ (f . n))

      proof

        let x be object;

        assume x in ( union ( rng (f | (n + 1))));

        then

        consider Y be set such that

         A14: x in Y and

         A15: Y in ( rng (f | (n + 1))) by TARSKI:def 4;

        consider X be object such that

         A16: X in ( dom (f | (n + 1))) and

         A17: ((f | (n + 1)) . X) = Y by A15, FUNCT_1:def 3;



         A18: X in (( dom f) /\ (n + 1)) by A16, RELAT_1: 61;

        then

         A19: X in ( Segm (n + 1)) by XBOOLE_0:def 4;



         A20: X in ( dom f) by A18, XBOOLE_0:def 4;

        reconsider X as Element of NAT by A19;

        X < (n + 1) by A19, NAT_1: 44;

        then

         A21: X <= n by NAT_1: 13;

        now

          per cases by A21, XXREAL_0: 1;

            suppose X < n;

            then X in ( Segm n) by NAT_1: 44;

            then X in (( dom f) /\ n) by A20, XBOOLE_0:def 4;

            then

             A22: X in ( dom (f | n)) by RELAT_1: 61;

            then

             A23: ((f | n) . X) in ( rng (f | n)) by FUNCT_1:def 3;



             A24: (f . X) = ((f | (n + 1)) . X) by A16, FUNCT_1: 47;

            ((f | n) . X) = (f . X) by A22, FUNCT_1: 47;

            then x in ( union ( rng (f | n))) by A14, A17, A24, A23, TARSKI:def 4;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose

             A25: X = n;

            (f . X) = ((f | (n + 1)) . X) by A16, FUNCT_1: 47;

            hence thesis by A14, A17, A25, XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

    end;

    scheme :: STIRL2_1:sch5

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

ex p be XFinSequence of D() st ( dom p) = ( Segm n()) & for k st k in ( Segm n()) holds P[k, (p . k)]

      provided

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



       A2: for k be object st k in n() holds ex x be object st x in D() & P[k, x]

      proof

        let k be object such that

         A3: k in n();

        n() is Subset of NAT by Th8;

        then

        reconsider k9 = k as Element of NAT by A3;

        ex x be Element of D() st P[k9, x] by A1, A3;

        hence thesis;

      end;

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

       A4: for x be object st x in n() holds P[x, (f . x)] from FUNCT_2:sch 1( A2);

      ( dom f) = n() by FUNCT_2:def 1;

      then

      reconsider p = f as XFinSequence of D() by AFINSQ_1: 5;

      take p;

      thus thesis by A4, FUNCT_2:def 1;

    end;

     Lm2:

    now

      let D be non empty set, F be XFinSequence of D;

      assume that

       A1: for i st i in ( dom F) holds (F . i) is finite and

       A2: for i, j st i in ( dom F) & j in ( dom F) & i <> j holds (F . i) misses (F . j);

      thus ex CardF be XFinSequence of NAT st ( dom CardF) = ( dom F) & (for i st i in ( dom CardF) holds (CardF . i) = ( card (F . i))) & ( card ( union ( rng F))) = ( Sum CardF)

      proof

        defpred FF[ Nat, set] means $2 = ( card (F . $1));



         A3: for k st k in ( Segm ( len F)) holds ex x be Element of NAT st FF[k, x]

        proof

          let k;

          assume k in ( Segm ( len F));

          then (F . k) is finite by A1;

          then

          reconsider m = ( card (F . k)) as Nat;

          ( card (F . k)) = ( card m);

          hence thesis;

        end;

        consider CardF be XFinSequence of NAT such that

         A4: ( dom CardF) = ( Segm ( len F)) & for k st k in ( Segm ( len F)) holds FF[k, (CardF . k)] from Sch6( A3);

        take CardF;

        thus ( dom CardF) = ( dom F) by A4;

        thus

         A5: for i st i in ( dom CardF) holds (CardF . i) = ( card (F . i)) by A4;



         A6: ( addnat "**" CardF) = ( Sum CardF) by AFINSQ_2: 51;

        per cases ;

          suppose

           A7: ( len CardF) = 0 ;

          then ( union ( rng F)) is empty by A4, RELAT_1: 42, ZFMISC_1: 2;

          hence thesis by A7, A6, AFINSQ_2:def 8, BINOP_2: 5;

        end;

          suppose

           A8: ( len CardF) <> 0 ;

          then

          consider f be sequence of NAT such that

           A9: (f . 0 ) = (CardF . 0 ) and

           A10: for n be Nat st (n + 1) < ( len CardF) holds (f . (n + 1)) = ( addnat . ((f . n),(CardF . (n + 1)))) and

           A11: ( addnat "**" CardF) = (f . (( len CardF) - 1)) by AFINSQ_2:def 8;

          defpred P[ Nat] means $1 < ( len CardF) implies ( card ( union ( rng (F | ($1 + 1))))) = (f . $1) & ( union ( rng (F | ($1 + 1)))) is finite;



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

          proof

            let k such that

             A13: P[k];

            set k1 = (k + 1);

            set Fk1 = (F | k1);

            set rFk1 = ( rng Fk1);

            assume that

             A14: k1 < ( len CardF);

            reconsider urFk1 = ( union rFk1) as finite set by A13, A14, NAT_1: 13;



             A15: (f . k1) = ( addnat . ((f . k),(CardF . k1))) by A10, A14;



             A16: ( union ( rng Fk1)) misses (F . k1)

            proof

              assume ( union ( rng Fk1)) meets (F . k1);

              then

              consider x be object such that

               A17: x in (( union ( rng Fk1)) /\ (F . k1)) by XBOOLE_0: 4;



               A18: x in (F . k1) by A17, XBOOLE_0:def 4;



               A19: k1 in ( dom F) by A4, A14, NAT_1: 44;

              x in ( union ( rng Fk1)) by A17, XBOOLE_0:def 4;

              then

              consider Y be set such that

               A20: x in Y and

               A21: Y in ( rng Fk1) by TARSKI:def 4;

              consider X be object such that

               A22: X in ( dom Fk1) and

               A23: (Fk1 . X) = Y by A21, FUNCT_1:def 3;

              reconsider X as Element of NAT by A22;



               A24: (Fk1 . X) = (F . X) by A22, FUNCT_1: 47;



               A25: X in (( dom F) /\ k1) by A22, RELAT_1: 61;

              then X in k1 by XBOOLE_0:def 4;

              then

               A26: X <> k1;

              X in ( dom F) by A25, XBOOLE_0:def 4;

              then Y misses (F . k1) by A2, A23, A19, A26, A24;

              hence contradiction by A20, A18, XBOOLE_0: 3;

            end;

            k1 in ( dom F) by A4, A14, NAT_1: 44;

            then

            reconsider Fk1 = (F . k1) as finite set by A1;

            k1 in ( len F) by A4, A14, NAT_1: 44;

            then ( card Fk1) = (CardF . k1) by A4;

            then

             A27: (f . k1) = ((f . k) + ( card Fk1)) by A15, BINOP_2:def 23;

            ( card (urFk1 \/ Fk1)) = ((f . k) + ( card Fk1)) by A13, A14, A16, CARD_2: 40, NAT_1: 13;

            hence thesis by A27, Th44;

          end;

          reconsider C1 = (( len CardF) - 1) as Element of NAT by A8, NAT_1: 20;



           A28: C1 < (C1 + 1) by NAT_1: 13;



           A29: (F | ( len CardF)) = F by A4;



           A30: P[ 0 ]

          proof

            assume 0 < ( len CardF);



             A31: ( union ( rng (F | ( 0 + 1)))) = (( union ( rng (F | 0 ))) \/ (F . 0 )) by Th44;



             A32: 0 in ( len CardF) by A8, AFINSQ_1: 86;



            thus ( card ( union ( rng (F | ( 0 + 1))))) = ( card ( {} \/ (F . 0 ))) by A31, ZFMISC_1: 2

            .= ( card (F . 0 ))

            .= (CardF . 0 ) by A32, A5

            .= (f . 0 ) by A9;

            hence ( union ( rng (F | ( 0 + 1)))) is finite;

          end;

          for k be Nat holds P[k] from NAT_1:sch 2( A30, A12);

          hence thesis by A11, A28, A29, A6;

        end;

      end;

    end;

    scheme :: STIRL2_1:sch6

    Sch8 { X,Y() -> finite set , x() -> set , P[ set], f() -> Function of ( card Y()), Y() } :

ex F be XFinSequence of NAT st ( dom F) = ( card Y()) & ( card { g where g be Function of X(), Y() : P[g] }) = ( Sum F) & for i st i in ( dom F) holds (F . i) = ( card { g where g be Function of X(), Y() : P[g] & (g . x()) = (f() . i) })

      provided

       A1: f() is onto one-to-one

       and

       A2: Y() is non empty

       and

       A3: x() in X();

      defpred FF[ Nat, set] means $2 = { g where g be Function of X(), Y() : P[g] & (g . x()) = (f() . $1) };

      set n = ( card Y());



       A4: for k st k in ( Segm n) holds ex x be Subset of ( Funcs (X(),Y())) st FF[k, x]

      proof

        let k such that k in ( Segm n);

        set F0 = { g where g be Function of X(), Y() : P[g] & (g . x()) = (f() . k) };

        F0 c= ( Funcs (X(),Y()))

        proof

          let x be object;

          assume x in F0;

          then ex g be Function of X(), Y() st x = g & P[g] & (g . x()) = (f() . k);

          hence thesis by A2, FUNCT_2: 8;

        end;

        hence thesis;

      end;

      consider F be XFinSequence of ( bool ( Funcs (X(),Y()))) such that

       A5: ( dom F) = ( Segm n) & for k st k in ( Segm n) holds FF[k, (F . k)] from Sch6( A4);



       A6: for i, j st i in ( dom F) & j in ( dom F) & i <> j holds (F . i) misses (F . j)

      proof

        let i, j such that

         A7: i in ( dom F) and

         A8: j in ( dom F) and

         A9: i <> j;

        assume (F . i) meets (F . j);

        then

        consider x be object such that

         A10: x in ((F . i) /\ (F . j)) by XBOOLE_0: 4;

        x in (F . i) by A10, XBOOLE_0:def 4;

        then x in { g where g be Function of X(), Y() : P[g] & (g . x()) = (f() . i) } by A5, A7;

        then

         A11: ex gi be Function of X(), Y() st x = gi & P[gi] & (gi . x()) = (f() . i);

        x in (F . j) by A10, XBOOLE_0:def 4;

        then x in { g where g be Function of X(), Y() : P[g] & (g . x()) = (f() . j) } by A5, A8;

        then

         A12: ex gj be Function of X(), Y() st x = gj & P[gj] & (gj . x()) = (f() . j);

        ( dom f()) = ( card Y()) by A2, FUNCT_2:def 1;

        hence contradiction by A1, A5, A7, A8, A9, A11, A12;

      end;



       A13: for i st i in ( dom F) holds (F . i) is finite

      proof

        let i;

        assume i in ( dom F);

        then

         A14: (F . i) in ( rng F) by FUNCT_1:def 3;



         A15: ( Funcs (X(),Y())) is finite by FRAENKEL: 6;

        thus thesis by A14, A15;

      end;

      consider CardF be XFinSequence of NAT such that

       A16: ( dom CardF) = ( dom F) and

       A17: for i st i in ( dom CardF) holds (CardF . i) = ( card (F . i)) and

       A18: ( card ( union ( rng F))) = ( Sum CardF) by Lm2, A13, A6;

      take CardF;

      thus ( dom CardF) = ( card Y()) by A5, A16;

      thus ( card { g where g be Function of X(), Y() : P[g] }) = ( Sum CardF)

      proof

        set G = { g where g be Function of X(), Y() : P[g] };



         A19: G c= ( union ( rng F))

        proof

          let x be object;

          assume x in G;

          then

          consider g be Function of X(), Y() such that

           A20: x = g and

           A21: P[g];



           A22: ( rng f()) = Y() by A1, FUNCT_2:def 3;

          ( dom g) = X() by A2, FUNCT_2:def 1;

          then (g . x()) in ( rng g) by A3, FUNCT_1:def 3;

          then

          consider y be object such that

           A23: y in ( dom f()) and

           A24: (f() . y) = (g . x()) by A22, FUNCT_1:def 3;

          (F . y) = { g1 where g1 be Function of X(), Y() : P[g1] & (g1 . x()) = (f() . y) } by A5, A23;

          then

           A25: g in (F . y) by A21, A24;

          (F . y) in ( rng F) by A5, A23, FUNCT_1:def 3;

          hence thesis by A20, A25, TARSKI:def 4;

        end;

        ( union ( rng F)) c= G

        proof

          let x be object;

          assume x in ( union ( rng F));

          then

          consider Y be set such that

           A26: x in Y and

           A27: Y in ( rng F) by TARSKI:def 4;

          consider X be object such that

           A28: X in ( dom F) and

           A29: (F . X) = Y by A27, FUNCT_1:def 3;

          Y = { g where g be Function of X(), Y() : P[g] & (g . x()) = (f() . X) } by A5, A28, A29;

          then ex gX be Function of X(), Y() st x = gX & P[gX] & (gX . x()) = (f() . X) by A26;

          hence thesis;

        end;

        hence thesis by A18, A19, XBOOLE_0:def 10;

      end;

      for i st i in ( dom CardF) holds (CardF . i) = ( card { g where g be Function of X(), Y() : P[g] & (g . x()) = (f() . i) })

      proof

        let i such that

         A30: i in ( dom CardF);

        (F . i) = { g where g be Function of X(), Y() : P[g] & (g . x()) = (f() . i) } by A5, A16, A30;

        hence thesis by A17, A30;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:45



     Th45: (k * (n block k)) = ( card { f where f be Function of ( Segm (n + 1)), ( Segm k) : f is onto "increasing & (f " {(f . n)}) <> {n} })

    proof

      now

        per cases ;

          suppose

           A1: k = 0 ;

          reconsider F1 = { f where f be Function of ( Segm (n + 1)), ( Segm k) : f is onto "increasing } as set;

          reconsider F = { f where f be Function of ( Segm (n + 1)), ( Segm k) : f is onto "increasing & (f " {(f . n)}) <> {n} } as set;



           A2: F c= F1

          proof

            let x be object;

            assume x in F;

            then ex f be Function of ( Segm (n + 1)), ( Segm k) st x = f & f is onto "increasing & (f " {(f . n)}) <> {n};

            hence thesis;

          end;

          ( card F1) = ((n + 1) block k);

          then F1 is empty by A1, Th31;

          hence thesis by A1, A2;

        end;

          suppose k > 0 ;

          then

           A3: ( Segm k) is non empty;

          set G1 = { g where g be Function of ( Segm (n + 1)), ( Segm k) : g is onto "increasing & (g " {(g . n)}) <> {n} };

          defpred P[ set] means ex f be Function of ( Segm (n + 1)), ( Segm k) st f = $1 & f is onto "increasing & (f " {(f . n)}) <> {n};

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

          then

           A4: n in ( Segm (n + 1)) by NAT_1: 44;

          consider f be Function such that

           A5: f is one-to-one and

           A6: ( dom f) = ( card k) and

           A7: ( rng f) = k by WELLORD2:def 4;

          reconsider f as Function of ( card ( Segm k)), ( Segm k) by A6, A7, FUNCT_2: 1;



           A8: f is onto one-to-one by A5, A7, FUNCT_2:def 3;

          consider F be XFinSequence of NAT such that

           A9: ( dom F) = ( card ( Segm k)) and

           A10: ( card { g where g be Function of ( Segm (n + 1)), ( Segm k) : P[g] }) = ( Sum F) and

           A11: for i st i in ( dom F) holds (F . i) = ( card { g where g be Function of ( Segm (n + 1)), ( Segm k) : P[g] & (g . n) = (f . i) }) from Sch8( A8, A3, A4);



           A12: for i be Nat st i in ( dom F) holds (F . i) = (n block k)

          proof

            set F2 = { g where g be Function of ( Segm n), ( Segm k) : g is onto "increasing };

            let i be Nat such that

             A13: i in ( dom F);



             A14: (f . i) in ( rng f) by A6, A9, A13, FUNCT_1:def 3;

            reconsider fi = (f . i) as Element of NAT by A7, A14;



             A15: fi < k by A14, NAT_1: 44;

            set F1 = { g where g be Function of ( Segm (n + 1)), ( Segm k) : P[g] & (g . n) = fi };

            set F = { g where g be Function of ( Segm (n + 1)), ( Segm k) : g is onto "increasing & (g " {(g . n)}) <> {n} & (g . n) = fi };



             A16: F1 c= F

            proof

              let x be object;

              assume x in F1;

              then ex g be Function of ( Segm (n + 1)), ( Segm k) st x = g & P[g] & (g . n) = fi;

              hence thesis;

            end;

            F c= F1

            proof

              let x be object;

              assume x in F;

              then ex g be Function of ( Segm (n + 1)), ( Segm k) st x = g & g is onto "increasing & (g " {(g . n)}) <> {n} & (g . n) = fi;

              hence thesis;

            end;

            then F = F1 by A16;

            then ( card F1) = ( card F2) by A15, Th43;

            hence thesis by A11, A13;

          end;

          then for i be Nat st i in ( dom F) holds (F . i) <= (n block k);

          then

           A17: ( Sum F) <= (( len F) * (n block k)) by AFINSQ_2: 59;

          set G = { g where g be Function of ( Segm (n + 1)), ( Segm k) : P[g] };



           A18: G1 c= G

          proof

            let x be object;

            assume x in G1;

            then ex g be Function of ( Segm (n + 1)), ( Segm k) st x = g & g is onto "increasing & (g " {(g . n)}) <> {n};

            hence thesis;

          end;



           A19: G c= G1

          proof

            let x be object;

            assume x in G;

            then ex g be Function of ( Segm (n + 1)), ( Segm k) st x = g & P[g];

            hence thesis;

          end;

          for i be Nat st i in ( dom F) holds (F . i) >= (n block k) by A12;

          then

           A20: ( Sum F) >= (( len F) * (n block k)) by AFINSQ_2: 60;

          ( Sum F) = (k * (n block k)) by A9, A17, A20, XXREAL_0: 1;

          hence thesis by A10, A18, A19, XBOOLE_0:def 10;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:46



     Th46: ((n + 1) block (k + 1)) = (((k + 1) * (n block (k + 1))) + (n block k))

    proof

      set F = { f where f be Function of ( Segm (n + 1)), ( Segm (k + 1)) : f is onto "increasing };

      set F1 = { f where f be Function of ( Segm (n + 1)), ( Segm (k + 1)) : f is onto "increasing & (f " {(f . n)}) = {n} };

      set F2 = { f where f be Function of ( Segm (n + 1)), ( Segm (k + 1)) : f is onto "increasing & (f " {(f . n)}) <> {n} };



       A1: F c= (F1 \/ F2)

      proof

        let x be object;

        assume x in F;

        then

        consider f be Function of ( Segm (n + 1)), ( Segm (k + 1)) such that

         A2: f = x and

         A3: f is onto "increasing;

        (f " {(f . n)}) = {n} or (f " {(f . n)}) <> {n};

        then f in F1 or f in F2 by A3;

        hence thesis by A2, XBOOLE_0:def 3;

      end;

      (F1 \/ F2) c= F

      proof

        let x be object;

        assume x in (F1 \/ F2);

        then x in F1 or x in F2 by XBOOLE_0:def 3;

        then (ex f be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f = x & f is onto "increasing & (f " {(f . n)}) = {n}) or ex f be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f = x & f is onto "increasing & (f " {(f . n)}) <> {n};

        hence thesis;

      end;

      then

       A4: (F1 \/ F2) = F by A1;



       A5: F1 misses F2

      proof

        assume F1 meets F2;

        then

        consider x be object such that

         A6: x in (F1 /\ F2) by XBOOLE_0: 4;

        x in F2 by A6, XBOOLE_0:def 4;

        then

         A7: ex f be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f = x & f is onto "increasing & (f " {(f . n)}) <> {n};

        x in F1 by A6, XBOOLE_0:def 4;

        then ex f be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f = x & f is onto "increasing & (f " {(f . n)}) = {n};

        hence contradiction by A7;

      end;



       A8: F2 c= ( Funcs ((n + 1),(k + 1)))

      proof

        let x be object;

        assume x in F2;

        then ex f be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f = x & f is onto "increasing & (f " {(f . n)}) <> {n};

        hence thesis by FUNCT_2: 8;

      end;



       A9: F1 c= ( Funcs ((n + 1),(k + 1)))

      proof

        let x be object;

        assume x in F1;

        then ex f be Function of ( Segm (n + 1)), ( Segm (k + 1)) st f = x & f is onto "increasing & (f " {(f . n)}) = {n};

        hence thesis by FUNCT_2: 8;

      end;

      ( Funcs ((n + 1),(k + 1))) is finite by FRAENKEL: 6;

      then

      reconsider F1, F2 as finite set by A9, A8;

      reconsider k1 = (k + 1) as Element of NAT ;



       A10: ( card F2) = (k1 * (n block k1)) by Th45;

      ( card F1) = (n block k) by Th42;

      hence thesis by A4, A5, A10, CARD_2: 40;

    end;

    theorem :: STIRL2_1:47



     Th47: n >= 1 implies (n block 2) = ((1 / 2) * ((2 |^ n) - 2))

    proof

      defpred P[ Nat] means ($1 block 2) = ((1 / 2) * ((2 |^ $1) - 2));



       A1: for k be Nat st k >= 1 & P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A2: k >= 1 and

         A3: P[k];

        ((k + 1) block 2) = ((2 * (k block (1 + 1))) + (k block 1)) by Th46

        .= ((2 * ((1 / 2) * ((2 |^ k) - 2))) + 1) by A2, A3, Th32

        .= ((1 / 2) * ((2 * (2 |^ k)) - 2))

        .= ((1 / 2) * ((2 |^ (k + 1)) - 2)) by NEWTON: 6;

        hence thesis;

      end;



       A4: P[1] by Th29;

      for k be Nat st k >= 1 holds P[k] from NAT_1:sch 8( A4, A1);

      hence thesis;

    end;

    theorem :: STIRL2_1:48



     Th48: n >= 2 implies (n block 3) = ((1 / 6) * (((3 |^ n) - (3 * (2 |^ n))) + 3))

    proof

      defpred P[ Nat] means ($1 block 3) = ((1 / 6) * (((3 |^ $1) - (3 * (2 |^ $1))) + 3));



       A1: for k be Nat st k >= 2 & P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A2: k >= 2 and

         A3: P[k];

        (k block 2) = ((1 / 2) * ((2 |^ k) - 2)) by A2, Th47, XXREAL_0: 2;



        hence ((k + 1) block 3) = ((3 * (k block (2 + 1))) + ((1 / 2) * ((2 |^ k) - 2))) by Th46

        .= ((1 / 6) * (((3 * (3 |^ k)) - ((3 * 2) * (2 |^ k))) + 3)) by A3

        .= ((1 / 6) * (((3 |^ (k + 1)) - (3 * (2 * (2 |^ k)))) + 3)) by NEWTON: 6

        .= ((1 / 6) * (((3 |^ (k + 1)) - (3 * (2 |^ (k + 1)))) + 3)) by NEWTON: 6;

      end;

      ((1 / 6) * (((3 |^ 2) - (3 * (2 |^ 2))) + 3)) = ((1 / 6) * (((3 * 3) - (3 * (2 |^ 2))) + 3)) by WSIERP_1: 1

      .= ((1 / 6) * (((3 * 3) - (3 * (2 * 2))) + 3)) by WSIERP_1: 1

      .= (2 block 3) by Th29;

      then

       A4: P[2];

      for k be Nat st k >= 2 holds P[k] from NAT_1:sch 8( A4, A1);

      hence thesis;

    end;



     Lm3: (n |^ 3) = ((n * n) * n)

    proof

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

      (n |^ (2 + 1)) = ((n |^ 2) * n) by NEWTON: 6

      .= ((n * n) * n) by WSIERP_1: 1;

      hence thesis;

    end;

    theorem :: STIRL2_1:49

    n >= 3 implies (n block 4) = ((1 / 24) * ((((4 |^ n) - (4 * (3 |^ n))) + (6 * (2 |^ n))) - 4))

    proof

      defpred P[ Nat] means ($1 block 4) = ((1 / 24) * ((((4 |^ $1) - (4 * (3 |^ $1))) + (6 * (2 |^ $1))) - 4));



       A1: for k be Nat st k >= 3 & P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A2: k >= 3 and

         A3: P[k];

        (k block 3) = ((1 / 6) * (((3 |^ k) - (3 * (2 |^ k))) + 3)) by A2, Th48, XXREAL_0: 2;



        hence ((k + 1) block 4) = ((4 * (k block (3 + 1))) + ((1 / 6) * (((3 |^ k) - (3 * (2 |^ k))) + 3))) by Th46

        .= ((1 / 24) * ((((4 * (4 |^ k)) - (4 * (3 * (3 |^ k)))) + (6 * (2 * (2 |^ k)))) - 4)) by A3

        .= ((1 / 24) * ((((4 |^ (k + 1)) - (4 * (3 * (3 |^ k)))) + (6 * (2 * (2 |^ k)))) - 4)) by NEWTON: 6

        .= ((1 / 24) * ((((4 |^ (k + 1)) - (4 * (3 |^ (k + 1)))) + (6 * (2 * (2 |^ k)))) - 4)) by NEWTON: 6

        .= ((1 / 24) * ((((4 |^ (k + 1)) - (4 * (3 |^ (k + 1)))) + (6 * (2 |^ (k + 1)))) - 4)) by NEWTON: 6;

      end;

      ((1 / 24) * ((((4 |^ 3) - (4 * (3 |^ 3))) + (6 * (2 |^ 3))) - 4)) = ((1 / 24) * (((((4 * 4) * 4) - (4 * (3 |^ 3))) + (6 * (2 |^ 3))) - 4)) by Lm3

      .= ((1 / 24) * (((64 - (4 * ((3 * 3) * 3))) + (6 * (2 |^ 3))) - 4)) by Lm3

      .= ((1 / 24) * (((64 - (4 * 27)) + (6 * ((2 * 2) * 2))) - 4)) by Lm3

      .= (3 block 4) by Th29;

      then

       A4: P[3];

      for k be Nat st k >= 3 holds P[k] from NAT_1:sch 8( A4, A1);

      hence thesis;

    end;

    theorem :: STIRL2_1:50



     Th50: (3 ! ) = 6 & (4 ! ) = 24

    proof



      thus

       A1: (3 ! ) = ((2 + 1) ! )

      .= (2 * 3) by NEWTON: 14, NEWTON: 15

      .= 6;



      thus (4 ! ) = ((3 + 1) ! )

      .= (6 * 4) by A1, NEWTON: 15

      .= 24;

    end;

    theorem :: STIRL2_1:51



     Th51: (n choose 1) = n & (n choose 2) = ((n * (n - 1)) / 2) & (n choose 3) = (((n * (n - 1)) * (n - 2)) / 6) & (n choose 4) = ((((n * (n - 1)) * (n - 2)) * (n - 3)) / 24)

    proof

      now

        (n = 0 or ... or n = 3) or 3 < n;

        per cases ;

          suppose n = 0 ;

          hence thesis by NEWTON:def 3;

        end;

          suppose n = 1;

          hence thesis by NEWTON: 21, NEWTON:def 3;

        end;

          suppose n = 2;

          hence thesis by NEWTON: 21, NEWTON: 23, NEWTON:def 3;

        end;

          suppose

           A1: n = 3;

          then

          reconsider n1 = (n - 1), n2 = (n - 2) as Element of NAT by NAT_1: 20;



           A2: ((n2 + 1) ! ) = ((n2 ! ) * (n2 + 1)) by NEWTON: 15;



           A3: ((n2 ! ) / (n2 ! )) = 1 by XCMPLX_1: 60;

          ((n1 + 1) ! ) = ((n1 ! ) * n) by NEWTON: 15;



          then (n choose 2) = (((n2 ! ) * ((n - 1) * n)) / ((n2 ! ) * (2 ! ))) by A1, A2, NEWTON:def 3

          .= ((((n2 ! ) / (n2 ! )) * ((n - 1) * n)) / 2) by NEWTON: 14, XCMPLX_1: 83

          .= (((n - 1) * n) / 2) by A3;

          hence thesis by A1, NEWTON: 21, NEWTON: 23, NEWTON:def 3;

        end;

          suppose

           A4: n > 3;

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

          then

          reconsider n1 = (n - 1), n2 = (n - 2), n3 = (n - 3), n4 = (n - 4) as Element of NAT by NAT_1: 21, XXREAL_0: 2;



           A5: ((n1 + 1) ! ) = ((n1 ! ) * n) by NEWTON: 15;



           A6: ((n2 + 1) ! ) = ((n2 ! ) * (n2 + 1)) by NEWTON: 15;



           A7: ((n2 ! ) / (n2 ! )) = 1 by XCMPLX_1: 60;

          n >= 2 by A4, XXREAL_0: 2;



          then

           A8: (n choose 2) = (((n2 ! ) * (n1 * n)) / ((n2 ! ) * (2 ! ))) by A5, A6, NEWTON:def 3

          .= ((((n2 ! ) / (n2 ! )) * (n1 * n)) / 2) by NEWTON: 14, XCMPLX_1: 83

          .= ((n * n1) / 2) by A7;



           A9: ((n4 ! ) / (n4 ! )) = 1 by XCMPLX_1: 60;



           A10: ((n4 + 1) ! ) = ((n4 ! ) * (n4 + 1)) by NEWTON: 15;



           A11: ((n3 ! ) / (n3 ! )) = 1 by XCMPLX_1: 60;



           A12: ((n3 + 1) ! ) = ((n3 ! ) * (n3 + 1)) by NEWTON: 15;



          then

           A13: (n choose 3) = (((n3 ! ) * ((n2 * n1) * n)) / ((n3 ! ) * (3 ! ))) by A4, A5, A6, NEWTON:def 3

          .= ((((n3 ! ) / (n3 ! )) * ((n2 * n1) * n)) / 6) by Th50, XCMPLX_1: 83

          .= (((n * n1) * n2) / 6) by A11;

          n >= (3 + 1) by A4, NAT_1: 13;



          then (n choose 4) = (((n4 ! ) * (((n3 * n2) * n1) * n)) / ((n4 ! ) * (4 ! ))) by A5, A6, A12, A10, NEWTON:def 3

          .= ((((n4 ! ) / (n4 ! )) * (((n3 * n2) * n1) * n)) / 24) by Th50, XCMPLX_1: 83

          .= ((((n * n1) * n2) * n3) / 24) by A9;

          hence thesis by A4, A8, A13, NEWTON: 23, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:52



     Th52: ((n + 1) block n) = ((n + 1) choose 2)

    proof

      defpred P[ Nat] means (($1 + 1) block $1) = (($1 + 1) choose 2);



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

      proof

        let k such that

         A2: P[k];

        set k1 = (k + 1);



        thus ((k1 + 1) block k1) = ((k1 * (k1 block k1)) + (k1 block k)) by Th46

        .= ((k1 * 1) + (k1 choose 2)) by A2, Th26

        .= (k1 + ((k1 * (k1 - 1)) / 2)) by Th51

        .= (((k1 + 1) * ((k1 + 1) - 1)) / 2)

        .= ((k1 + 1) choose 2) by Th51;

      end;

      (1 block 0 ) = 0 by Th31;

      then

       A3: P[ 0 ] by NEWTON:def 3;

      for k holds P[k] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: STIRL2_1:53

    ((n + 2) block n) = ((3 * ((n + 2) choose 4)) + ((n + 2) choose 3))

    proof

      defpred P[ Nat] means (($1 + 2) block $1) = ((3 * (($1 + 2) choose 4)) + (($1 + 2) choose 3));



       A1: (2 choose 3) = 0 by NEWTON:def 3;



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

      proof

        let k such that

         A3: P[k];

        set k1 = (k + 1);

        set k2 = (k + 2);

        set k3 = (k2 + 1);



         A4: (k1 * ((k1 + 1) block k1)) = (k1 * (k2 choose 2)) by Th52

        .= (k1 * ((k2 * (k2 - 1)) / 2)) by Th51

        .= ((k2 * (k2 - 1)) * ((k1 * 12) / 24));

        (k2 block k) = ((3 * ((((k2 * (k2 - 1)) * (k2 - 2)) * (k2 - 3)) / 24)) + (k2 choose 3)) by A3, Th51

        .= ((3 * ((((k2 * (k2 - 1)) * (k2 - 2)) * (k2 - 3)) / 24)) + (((k2 * (k2 - 1)) * (k2 - 2)) / 6)) by Th51

        .= ((k2 * (k2 - 1)) * ((((3 * (k2 - 2)) * (k2 - 3)) / 24) + ((4 * (k2 - 2)) / 24)));



        then (k3 block k1) = (((k2 * k1) * ((k1 * 12) / 24)) + ((k2 * k1) * ((((3 * k) * (k2 - 3)) / 24) + ((4 * k) / 24)))) by A4, Th46

        .= ((3 * ((((k3 * (k3 - 1)) * (k3 - 2)) * (k3 - 3)) / 24)) + (((k3 * k2) * k1) / 6))

        .= ((3 * (k3 choose 4)) + (((k3 * (k3 - 1)) * (k3 - 2)) / 6)) by Th51

        .= ((3 * (k3 choose 4)) + (k3 choose 3)) by Th51;

        hence thesis;

      end;

      (2 choose 4) = 0 by NEWTON:def 3;

      then

       A5: P[ 0 ] by A1, Th31;

      for k holds P[k] from NAT_1:sch 2( A5, A2);

      hence thesis;

    end;

    theorem :: STIRL2_1:54



     Th54: for F be Function, y holds ( rng (F | (( dom F) \ (F " {y})))) = (( rng F) \ {y}) & for x st x <> y holds ((F | (( dom F) \ (F " {y}))) " {x}) = (F " {x})

    proof

      let F be Function, y;

      set D = (( dom F) \ (F " {y}));



       A1: ( rng (F | D)) c= (( rng F) \ {y})

      proof

        let Fx be object;

        assume Fx in ( rng (F | D));

        then

        consider x be object such that

         A2: x in ( dom (F | D)) and

         A3: Fx = ((F | D) . x) by FUNCT_1:def 3;



         A4: x in (( dom F) /\ D) by A2, RELAT_1: 61;

        then x in ((( dom F) /\ ( dom F)) \ (F " {y})) by XBOOLE_1: 49;

        then not x in (F " {y}) by XBOOLE_0:def 5;

        then not (F . x) in {y} by A4, FUNCT_1:def 7;

        then

         A5: not Fx in {y} by A2, A3, FUNCT_1: 47;

        (F . x) in ( rng F) by A4, FUNCT_1:def 3;

        then Fx in ( rng F) by A2, A3, FUNCT_1: 47;

        hence thesis by A5, XBOOLE_0:def 5;

      end;

      (( rng F) \ {y}) c= ( rng (F | D))

      proof

        let Fx be object such that

         A6: Fx in (( rng F) \ {y});

        consider x be object such that

         A7: x in ( dom F) and

         A8: (F . x) = Fx by A6, FUNCT_1:def 3;

         not Fx in {y} by A6, XBOOLE_0:def 5;

        then not x in (F " {y}) by A8, FUNCT_1:def 7;

        then x in D by A7, XBOOLE_0:def 5;

        then x in (( dom F) /\ D) by XBOOLE_0:def 4;

        then

         A9: x in ( dom (F | D)) by RELAT_1: 61;

        then ((F | D) . x) in ( rng (F | D)) by FUNCT_1:def 3;

        hence thesis by A8, A9, FUNCT_1: 47;

      end;

      hence ( rng (F | D)) = (( rng F) \ {y}) by A1;

      let x such that

       A10: x <> y;

      now

        let z be object such that

         A11: z in (F " {x});

        (F . z) in {x} by A11, FUNCT_1:def 7;

        then (F . z) <> y by A10, TARSKI:def 1;

        then not (F . z) in {y} by TARSKI:def 1;

        then

         A12: not z in (F " {y}) by FUNCT_1:def 7;

        z in ( dom F) by A11, FUNCT_1:def 7;

        hence z in (( dom F) \ (F " {y})) by A12, XBOOLE_0:def 5;

      end;

      then (F " {x}) c= D;

      hence thesis by FUNCT_2: 98;

    end;

    theorem :: STIRL2_1:55



     Th55: ( card X) = (k + 1) & x in X implies ( card (X \ {x})) = k

    proof

      assume that

       A1: ( card X) = (k + 1) and

       A2: x in X;

      reconsider X9 = X as finite set by A1;

      set Xx = (X9 \ {x});

       {x} c= X by A2, ZFMISC_1: 31;

      then ( {x} /\ X) = {x} by XBOOLE_1: 28;

      then (Xx \/ {x}) = X by XBOOLE_1: 51;

      then

       A3: (( card {x}) + ( card Xx)) = (k + 1) by A1, CARD_2: 40, XBOOLE_1: 79;

      ( card {x}) = 1 by CARD_1: 30;

      hence thesis by A3;

    end;

    scheme :: STIRL2_1:sch7

    Sch9 { P[ set], Q[ set, Function] } :

for F be Function st ( rng F) is finite holds P[F]

      provided

       A1: P[ {} ]

       and

       A2: for F be Function st for x st x in ( rng F) & Q[x, F] holds P[(F | (( dom F) \ (F " {x})))] holds P[F];

      defpred R[ Nat] means for F be Function st ( card ( rng F)) = $1 holds P[F];



       A3: for n st R[n] holds R[(n + 1)]

      proof

        let n such that

         A4: R[n];

        let F be Function such that

         A5: ( card ( rng F)) = (n + 1);

        for x st x in ( rng F) & Q[x, F] holds P[(F | (( dom F) \ (F " {x})))]

        proof

          let x such that

           A6: x in ( rng F) and Q[x, F];

          set D = (( dom F) \ (F " {x}));

          ( card (( rng F) \ {x})) = n by A5, A6, Th55;

          then ( card ( rng (F | D))) = n by Th54;

          hence thesis by A4;

        end;

        hence thesis by A2;

      end;

      let F be Function;

      assume ( rng F) is finite;

      then

      reconsider n = ( card ( rng F)) as Nat;



       A7: ( card ( rng F)) = n;



       A8: R[ 0 ]

      proof

        let F be Function;

        assume ( card ( rng F)) = 0 ;

        then ( rng F) = {} ;

        hence thesis by A1, RELAT_1: 41;

      end;

      for k holds R[k] from NAT_1:sch 2( A8, A3);

      hence thesis by A7;

    end;

    theorem :: STIRL2_1:56



     Th56: for N be Subset of NAT st N is finite holds ex k st for n st n in N holds n <= k

    proof

      let N be Subset of NAT ;

      assume N is finite;

      then

      reconsider n = ( card N) as Nat;



       A1: (N,n) are_equipotent by CARD_1:def 2;

      consider F be Function such that F is one-to-one and

       A2: ( dom F) = n and

       A3: ( rng F) = N by A1, WELLORD2:def 4;

      reconsider F as XFinSequence by A2, AFINSQ_1: 5;

      reconsider F as XFinSequence of NAT by A3, RELAT_1:def 19;

      reconsider k = ( Sum F) as Element of NAT by ORDINAL1:def 12;

      take k;

      let n such that

       A4: n in N;

      F <> 0 by A3, A4;

      then

       A5: ( len F) > 0 ;

      ex x be object st x in ( dom F) & (F . x) = n by A3, A4, FUNCT_1:def 3;

      hence thesis by A5, AFINSQ_2: 61;

    end;

    theorem :: STIRL2_1:57



     Th57: for X, Y holds for x,y be object st (Y is empty implies X is empty) & not x in X holds for F be Function of X, Y holds ex G be Function of (X \/ {x}), (Y \/ {y}) st (G | X) = F & (G . x) = y

    proof

      let X, Y;

      let x,y be object such that

       A1: Y is empty implies X is empty and

       A2: not x in X;

      set Y1 = (Y \/ {y});

      set X1 = (X \/ {x});

      deffunc F( set) = y;

      let F be Function of X, Y;

      y in {y} by TARSKI:def 1;

      then

       A3: for x9 be set st x9 in (X1 \ X) holds F(x9) in Y1 by XBOOLE_0:def 3;



       A4: X c= X1 & Y c= Y1 by XBOOLE_1: 7;

      consider G be Function of X1, Y1 such that

       A5: (G | X) = F & for x9 be set st x9 in (X1 \ X) holds (G . x9) = F(x9) from Sch2( A3, A4, A1);

      x in {x} by TARSKI:def 1;

      then x in X1 by XBOOLE_0:def 3;

      then x in (X1 \ X) by A2, XBOOLE_0:def 5;

      then (G . x) = y by A5;

      hence thesis by A5;

    end;

    theorem :: STIRL2_1:58



     Th58: for X, Y, x, y st (Y is empty implies X is empty) holds for F be Function of X, Y, G be Function of (X \/ {x}), (Y \/ {y}) st (G | X) = F & (G . x) = y holds (F is onto implies G is onto) & ( not y in Y & F is one-to-one implies G is one-to-one)

    proof

      let X, Y, x, y such that

       A1: Y is empty implies X is empty;

      let F be Function of X, Y, G be Function of (X \/ {x}), (Y \/ {y}) such that

       A2: (G | X) = F and

       A3: (G . x) = y;

      thus F is onto implies G is onto

      proof

        assume

         A4: F is onto;

        (Y \/ {y}) c= ( rng G)

        proof

          let Fx be object such that

           A5: Fx in (Y \/ {y});

          now

            per cases by A5, XBOOLE_0:def 3;

              suppose Fx in Y;

              then Fx in ( rng F) by A4, FUNCT_2:def 3;

              then

              consider x9 be object such that

               A6: x9 in ( dom F) and

               A7: (F . x9) = Fx by FUNCT_1:def 3;



               A8: x9 in X by A6;



               A9: ( dom G) = (X \/ {x}) by FUNCT_2:def 1;



               A10: X c= (X \/ {x}) by XBOOLE_1: 7;

              (G . x9) = (F . x9) by A2, A6, FUNCT_1: 47;

              hence thesis by A7, A8, A10, A9, FUNCT_1:def 3;

            end;

              suppose

               A11: Fx in {y};



               A12: ( dom G) = (X \/ {x}) by FUNCT_2:def 1;



               A13: {x} c= (X \/ {x}) by XBOOLE_1: 7;



               A14: x in {x} by TARSKI:def 1;

              Fx = y by A11, TARSKI:def 1;

              hence thesis by A3, A12, A14, A13, FUNCT_1:def 3;

            end;

          end;

          hence thesis;

        end;

        then (Y \/ {y}) = ( rng G);

        hence thesis by FUNCT_2:def 3;

      end;

      thus not y in Y & F is one-to-one implies G is one-to-one

      proof

        assume that

         A15: not y in Y and

         A16: F is one-to-one;

        let x1,x2 be object such that

         A17: x1 in ( dom G) and

         A18: x2 in ( dom G) and

         A19: (G . x1) = (G . x2);



         A20: for x9 be set st x9 in X holds x9 in ( dom F) & (F . x9) = (G . x9) & (G . x9) <> y

        proof

          let x9 be set such that

           A21: x9 in X;



           A22: x9 in ( dom F) by A1, A21, FUNCT_2:def 1;

          then

           A23: (F . x9) in ( rng F) by FUNCT_1:def 3;

          (F . x9) = (G . x9) by A2, A22, FUNCT_1: 47;

          hence thesis by A15, A21, A23, FUNCT_2:def 1;

        end;

        now

          per cases by A17, A18, XBOOLE_0:def 3;

            suppose

             A24: x1 in X & x2 in X;

            then

             A25: (F . x1) = (G . x1) by A20;



             A26: x2 in ( dom F) by A20, A24;



             A27: (F . x2) = (G . x2) by A20, A24;

            x1 in ( dom F) by A20, A24;

            hence thesis by A16, A19, A26, A25, A27;

          end;

            suppose

             A28: x1 in X & x2 in {x};

            then (G . x2) = y by A3, TARSKI:def 1;

            hence thesis by A19, A20, A28;

          end;

            suppose

             A29: x1 in {x} & x2 in X;

            then (G . x1) = y by A3, TARSKI:def 1;

            hence thesis by A19, A20, A29;

          end;

            suppose

             A30: x1 in {x} & x2 in {x};

            then x = x1 by TARSKI:def 1;

            hence thesis by A30, TARSKI:def 1;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: STIRL2_1:59



     Th59: for N be finite Subset of NAT holds ex Order be Function of N, ( Segm ( card N)) st Order is bijective & for n, k st n in ( dom Order) & k in ( dom Order) & n < k holds (Order . n) < (Order . k)

    proof

      defpred P[ Nat] means for N be finite Subset of NAT st ( card N) = $1 holds ex F be Function of N, ( Segm ( card N)) st F is bijective & for n, k st n in ( dom F) & k in ( dom F) & n < k holds (F . n) < (F . k);



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

      proof

        let k such that

         A2: P[k];

        let N be finite Subset of NAT such that

         A3: ( card N) = (k + 1);

        defpred M[ set] means $1 in N;

        ex x be object st x in N by A3, CARD_1: 27, XBOOLE_0:def 1;

        then

         A4: ex n be Nat st M[n];

        consider m9 be Nat such that

         A5: for n st n in N holds n <= m9 by Th56;



         A6: for n be Nat st M[n] holds n <= m9 by A5;

        consider m be Nat such that

         A7: M[m] & for n be Nat st M[n] holds n <= m from NAT_1:sch 6( A6, A4);

        set Nm = (N \ {m});

        consider F be Function of Nm, ( Segm ( card Nm)) such that

         A8: F is bijective and

         A9: for n, k st n in ( dom F) & k in ( dom F) & n < k holds (F . n) < (F . k) by A2, A3, A7, Th55;



         A10: ( card Nm) = k by A3, A7, Th55;



         A11: (( Segm k) \/ {k}) = ( Segm (k + 1)) by AFINSQ_1: 2;



         A12: ( card Nm) is empty implies Nm is empty;

        m in {m} by TARSKI:def 1;

        then not m in Nm by XBOOLE_0:def 5;

        then

        consider G be Function of (Nm \/ {m}), (( card Nm) \/ {k}) such that

         A13: (G | Nm) = F and

         A14: (G . m) = k by A12, Th57;

        N = (Nm \/ {m}) by A7, ZFMISC_1: 116;

        then

        reconsider G9 = G as Function of N, ( Segm ( card N)) by A3, A10, A11;

        take G9;

         not k in ( card Nm) by A10;

        then G is one-to-one onto by A8, A12, A13, A14, Th58;

        hence G9 is bijective by A11, A3, A10;

        thus for n, k st n in ( dom G9) & k in ( dom G9) & n < k holds (G9 . n) < (G9 . k)

        proof



           A15: for i st i in Nm holds i < m & (G9 . i) < k

          proof

            let i such that

             A16: i in Nm;

             not i in {m} by A16, XBOOLE_0:def 5;

            then

             A17: i <> m by TARSKI:def 1;

             M[i] by A16, XBOOLE_0:def 5;

            then i <= m by A7;

            hence i < m by A17, XXREAL_0: 1;



             A18: i in ( dom F) by A16, FUNCT_2:def 1;

            then

             A19: (F . i) = (G9 . i) by A13, FUNCT_1: 47;



             A20: (F . i) in ( card Nm) by A18, FUNCT_2: 5;

            ( card Nm) = k by A3, A7, Th55;

            hence (G9 . i) < k by A19, NAT_1: 44, A20;

          end;

          let i, j such that

           A21: i in ( dom G9) and

           A22: j in ( dom G9) and

           A23: i < j;



           A24: ( dom G9) = (Nm \/ {m}) by FUNCT_2:def 1;

          now

            per cases by A21, A22, A24, XBOOLE_0:def 3;

              suppose

               A25: i in Nm & j in Nm;

              then

               A26: j in ( dom F) by FUNCT_2:def 1;

              then

               A27: (F . j) = (G9 . j) by A13, FUNCT_1: 47;



               A28: i in ( dom F) by A25, FUNCT_2:def 1;

              then (F . i) = (G9 . i) by A13, FUNCT_1: 47;

              hence thesis by A9, A23, A28, A26, A27;

            end;

              suppose

               A29: i in Nm & j in {m};

              then (G9 . i) < k by A15;

              hence thesis by A14, A29, TARSKI:def 1;

            end;

              suppose

               A30: i in {m} & j in Nm;

              then i = m by TARSKI:def 1;

              hence thesis by A23, A15, A30;

            end;

              suppose

               A31: i in {m} & j in {m};

              then i = m by TARSKI:def 1;

              hence thesis by A23, A31, TARSKI:def 1;

            end;

          end;

          hence thesis;

        end;

      end;



       A32: P[ 0 ]

      proof

        set P = {} ;



         A33: ( rng P) = {} ;

        let N be finite Subset of NAT such that

         A34: ( card N) = 0 ;

        N is empty by A34;

        then

        reconsider P as Function of N, ( Segm ( card N)) by A33, FUNCT_2: 1;

        take P;

        ( rng P) = {} ;

        then P is one-to-one onto by A34, FUNCT_2:def 3;

        hence P is bijective;

        thus thesis;

      end;

      for k holds P[k] from NAT_1:sch 2( A32, A1);

      hence thesis;

    end;

    ::$Canceled



     Th60: for X,Y be finite set, F be Function of X, Y st ( card X) = ( card Y) holds F is onto iff F is one-to-one by FINSEQ_4: 63;



     Lm5: for n be Element of NAT , N be finite Subset of NAT , F be Function of N, ( Segm ( card N)) st n in N & F is bijective & for n, k st n in ( dom F) & k in ( dom F) & n < k holds (F . n) < (F . k) holds ex P be Permutation of N st for k st k in N holds (k < n implies (P . k) = ((F " ) . ((F . k) + 1))) & (k = n implies (P . k) = ((F " ) . 0 )) & (k > n implies (P . k) = k)

    proof

      let n be Element of NAT , N be finite Subset of NAT , F be Function of N, ( Segm ( card N)) such that

       A1: n in N and

       A2: F is bijective and

       A3: for n, k st n in ( dom F) & k in ( dom F) & n < k holds (F . n) < (F . k);

      ( rng F) = ( card N) by A2, FUNCT_2:def 3;

      then

      reconsider F9 = (F " ) as Function of ( card N), N by A2, FUNCT_2: 25;

      defpred P[ object, object] means for k st k = $1 holds (k < n implies $2 = ((F " ) . ((F . k) + 1))) & (k = n implies $2 = ((F " ) . 0 )) & (k > n implies $2 = k);



       A4: ( dom F) = N by A1, FUNCT_2:def 1;



       A5: ( dom F9) = ( card N) by A1, FUNCT_2:def 1;



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

      proof

        let x9 be object such that

         A7: x9 in N;

        reconsider x = x9 as Element of NAT by A7;

        now

          per cases by XXREAL_0: 1;

            suppose

             A8: x < n;

            then (F . x) < (F . n) by A1, A3, A4, A7;

            then

             A9: ((F . x) + 1) <= (F . n) by NAT_1: 13;

            n in ( dom F) by A1, A4;

            then (F . n) in ( card N) by FUNCT_2: 5;

            then (F . n) < ( card N) by NAT_1: 44;

            then ((F . x) + 1) < ( card N) by A9, XXREAL_0: 2;

            then ((F . x) + 1) in ( dom F9) by A5, NAT_1: 44;

            then

             A10: (F9 . ((F . x) + 1)) in ( rng F9) by FUNCT_1:def 3;

            set FF = ((F " ) . ((F . x) + 1));

             P[x9, FF] by A8;

            hence thesis by A10;

          end;

            suppose

             A11: x = n;

             0 in ( dom F9) by A1, A5, NAT_1: 44;

            then

             A12: (F9 . 0 ) in ( rng F9) by FUNCT_1:def 3;

             P[x9, ((F " ) . 0 )] by A11;

            hence thesis by A12;

          end;

            suppose x > n;

            then P[x, x];

            hence thesis by A7;

          end;

        end;

        hence thesis;

      end;

      consider P be Function of N, N such that

       A13: for x be object st x in N holds P[x, (P . x)] from FUNCT_2:sch 1( A6);

      N c= ( rng P)

      proof

        let Px9 be object such that

         A14: Px9 in N;

        reconsider Px = Px9 as Element of NAT by A14;

        now

          per cases ;

            suppose

             A15: Px <= n;

            ( rng F9) = N by A2, A4, FUNCT_1: 33;

            then

            consider x be object such that

             A16: x in ( dom F9) and

             A17: (F9 . x) = Px by A14, FUNCT_1:def 3;

            reconsider x as Element of NAT by A5, A16;

            now

              per cases ;

                suppose

                 A18: x = 0 ;



                 A19: ( dom P) = N by A1, FUNCT_2:def 1;

                (P . n) = ((F " ) . 0 ) by A1, A13;

                hence thesis by A1, A17, A18, A19, FUNCT_1:def 3;

              end;

                suppose x > 0 ;

                then

                reconsider x1 = (x - 1) as Element of NAT by NAT_1: 20;



                 A20: x1 < (x1 + 1) by NAT_1: 13;

                x < ( card N) by A16, NAT_1: 44;

                then x1 < ( card N) by A20, XXREAL_0: 2;

                then

                 A21: x1 in ( Segm ( card N)) by NAT_1: 44;

                ( card N) = ( rng F) by A2, FUNCT_2:def 3;

                then

                consider y be object such that

                 A22: y in ( dom F) and

                 A23: (F . y) = x1 by A21, FUNCT_1:def 3;

                reconsider y as Element of NAT by A4, A22;



                 A24: y in ( dom P) by A4, A22, FUNCT_2:def 1;



                 A25: y < n

                proof

                  assume y >= n;

                  then y > n or y = n by XXREAL_0: 1;

                  then

                   A26: x1 >= (F . n) by A1, A3, A4, A22, A23;

                  x in ( rng F) by A2, A16, FUNCT_1: 33;

                  then

                   A27: (F . Px) = x by A2, A17, FUNCT_1: 32;

                  Px < n or Px = n by A15, XXREAL_0: 1;

                  then

                   A28: (F . Px) <= (F . n) by A1, A3, A4, A14;

                  (x1 + 1) > x1 by NAT_1: 13;

                  hence contradiction by A26, A27, A28, XXREAL_0: 2;

                end;

                ((F " ) . ((F . y) + 1)) = Px by A17, A23;

                then (P . y) = Px by A13, A22, A25;

                hence thesis by A24, FUNCT_1:def 3;

              end;

            end;

            hence thesis;

          end;

            suppose

             A29: Px > n;



             A30: Px in ( dom P) by A14, FUNCT_2:def 1;

            Px = (P . Px) by A13, A14, A29;

            hence thesis by A30, FUNCT_1:def 3;

          end;

        end;

        hence thesis;

      end;

      then N = ( rng P);

      then

       A31: P is onto by FUNCT_2:def 3;

      ( card N) = ( card N);

      then P is onto one-to-one by A31, Th60;

      then

      reconsider P as Permutation of N;

      take P;

      thus thesis by A13;

    end;

    theorem :: STIRL2_1:61



     Th61: for F,G be Function, y st y in ( rng (G * F)) & G is one-to-one holds ex x st x in ( dom G) & x in ( rng F) & (G " {y}) = {x} & (F " {x}) = ((G * F) " {y})

    proof

      let F,G be Function, y such that

       A1: y in ( rng (G * F)) and

       A2: G is one-to-one;

      consider x be object such that

       A3: x in ( dom (G * F)) and

       A4: ((G * F) . x) = y by A1, FUNCT_1:def 3;



       A5: (F . x) in ( dom G) by A3, FUNCT_1: 11;



       A6: (G . (F . x)) = y by A3, A4, FUNCT_1: 12;

      then (G . (F . x)) in {y} by TARSKI:def 1;

      then

       A7: (F . x) in (G " {y}) by A5, FUNCT_1:def 7;



       A8: (F " {(F . x)}) c= ((G * F) " {y})

      proof

        let d be object such that

         A9: d in (F " {(F . x)});



         A10: d in ( dom F) by A9, FUNCT_1:def 7;

        (F . d) in {(F . x)} by A9, FUNCT_1:def 7;

        then

         A11: (F . d) = (F . x) by TARSKI:def 1;

        then (G . (F . d)) in {y} by A6, TARSKI:def 1;

        then

         A12: ((G * F) . d) in {y} by A10, FUNCT_1: 13;

        d in ( dom (G * F)) by A5, A10, A11, FUNCT_1: 11;

        hence thesis by A12, FUNCT_1:def 7;

      end;

      y in ( rng G) by A1, FUNCT_1: 14;

      then

      consider Fx be object such that

       A13: (G " {y}) = {Fx} by A2, FUNCT_1: 74;

      x in ( dom F) by A3, FUNCT_1: 11;

      then

       A14: (F . x) in ( rng F) by FUNCT_1:def 3;



       A15: (F . x) in ( dom G) by A3, FUNCT_1: 11;

      ((G * F) " {y}) c= (F " {(F . x)})

      proof

        let d be object such that

         A16: d in ((G * F) " {y});



         A17: d in ( dom (G * F)) by A16, FUNCT_1:def 7;

        then

         A18: d in ( dom F) by FUNCT_1: 11;

        ((G * F) . d) in {y} by A16, FUNCT_1:def 7;

        then

         A19: (G . (F . d)) in {y} by A17, FUNCT_1: 12;



         A20: (F . d) in ( dom G) by A17, FUNCT_1: 11;

        (F . x) = Fx by A13, A7, TARSKI:def 1;

        then (F . d) in {(F . x)} by A13, A20, A19, FUNCT_1:def 7;

        hence thesis by A18, FUNCT_1:def 7;

      end;

      then

       A21: (F " {(F . x)}) = ((G * F) " {y}) by A8;

      (G " {y}) = {(F . x)} by A13, A7, TARSKI:def 1;

      hence thesis by A15, A14, A21;

    end;

    definition

      let Ne, Ke;

      let f be Function of Ne, Ke;

      :: STIRL2_1:def3

      attr f is 'increasing means for l, m st l in ( rng f) & m in ( rng f) & l < m holds ( min* (f " {l})) < ( min* (f " {m}));

    end

    theorem :: STIRL2_1:62



     Th62: for F be Function of Ne, Ke st F is 'increasing holds ( min* ( rng F)) = (F . ( min* ( dom F)))

    proof

      let F be Function of Ne, Ke such that

       A1: F is 'increasing;

      now

        per cases ;

          suppose

           A2: ( rng F) is empty;

          then

           A3: ( min* ( rng F)) = 0 by NAT_1:def 1;

          ( dom F) = {} by A2, RELAT_1: 42;

          hence thesis by A3, FUNCT_1:def 2;

        end;

          suppose

           A4: ( rng F) is non empty;

          then

          reconsider rngF = ( rng F), Ke as non empty Subset of NAT by XBOOLE_1: 1;

          reconsider domF = ( dom F) as non empty Subset of NAT by A4, FUNCT_2:def 1, RELAT_1: 42;

          set md = ( min* domF);

          set mr = ( min* rngF);

          mr = (F . md)

          proof



             A5: md in ( dom F) by NAT_1:def 1;

            then (F . md) in rngF by FUNCT_1:def 3;

            then

             A6: mr <= (F . md) by NAT_1:def 1;

            assume mr <> (F . md);

            then

             A7: mr < (F . md) by A6, XXREAL_0: 1;



             A8: md in domF by NAT_1:def 1;



             A9: md in ( dom F) by NAT_1:def 1;

            mr in rngF by NAT_1:def 1;

            then

            consider x be object such that

             A10: x in ( dom F) and

             A11: (F . x) = mr by FUNCT_1:def 3;



             A12: (F . md) in {(F . md)} by TARSKI:def 1;

            (F . x) in {mr} by A11, TARSKI:def 1;

            then

            reconsider Fmr = (F " {mr}), Fmd = (F " {(F . md)}) as non empty Subset of NAT by A10, A12, A9, FUNCT_1:def 7, XBOOLE_1: 1;



             A13: mr in rngF by NAT_1:def 1;

            ( min* Fmr) in Fmr by NAT_1:def 1;

            then ( min* Fmr) in domF by FUNCT_1:def 7;

            then

             A14: ( min* Fmr) >= md by NAT_1:def 1;

            (F . md) in {(F . md)} by TARSKI:def 1;

            then md in Fmd by A8, FUNCT_1:def 7;

            then

             A15: md >= ( min* Fmd) by NAT_1:def 1;

            (F . md) in ( rng F) by A5, FUNCT_1:def 3;

            then ( min* (F " {mr})) < ( min* (F " {(F . md)})) by A1, A7, A13;

            hence contradiction by A14, A15, XXREAL_0: 2;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: STIRL2_1:63

    for F be Function of Ne, Ke st ( rng F) is finite holds ex I be Function of Ne, Ke, P be Permutation of ( rng F) st F = (P * I) & ( rng F) = ( rng I) & I is 'increasing

    proof

      defpred Q[ set, Function] means $1 = ($2 . ( min* ( dom $2)));

      defpred P[ set] means for Ne,Ke be Subset of NAT , F be Function of Ne, Ke st F = $1 & ( rng F) is finite holds ex P be Permutation of ( rng F), G be Function of Ne, Ke st F = (P * G) & ( rng F) = ( rng G) & for i, j st i in ( rng G) & j in ( rng G) & i < j holds ( min* (G " {i})) < ( min* (G " {j}));



       A1: P[ {} ]

      proof

        let Ne,Me be Subset of NAT , F be Function of Ne, Me such that

         A2: F = {} and ( rng F) is finite;

        reconsider R = ( rng F) as empty set by A2;

        set P = {} ;



         A3: ( rng P) = {} ;

        reconsider P as Function of R, R by A3, FUNCT_2: 1;

        ( rng R) = {} ;

        then P is one-to-one onto by FUNCT_2:def 3;

        then

        reconsider P as Permutation of ( rng F);

        take P, F;

        ( rng F) = R;

        then F = {} ;

        hence thesis;

      end;



       A4: for F be Function st for x st x in ( rng F) & Q[x, F] holds P[(F | (( dom F) \ (F " {x})))] holds P[F]

      proof

        let F9 be Function such that

         A5: for x st x in ( rng F9) & Q[x, F9] holds P[(F9 | (( dom F9) \ (F9 " {x})))];

        let N,K be Subset of NAT , F be Function of N, K such that

         A6: F = F9 and

         A7: ( rng F) is finite;

        now

          per cases ;

            suppose ( rng F9) is empty;

            then F9 = {} ;

            hence thesis by A1, A6;

          end;

            suppose

             A8: ( rng F9) is non empty;

            then

            reconsider domF = ( dom F) as non empty Subset of NAT by A6, RELAT_1: 42, XBOOLE_1: 1;

            reconsider K as non empty Subset of NAT by A6, A8;

            set m = ( min* domF);

            set D = (( dom F) \ (F " {(F . m)}));

            ( min* domF) in domF by NAT_1:def 1;

            then

             A9: (F . m) in ( rng F) by FUNCT_1:def 3;

            now

              per cases ;

                suppose ( rng (F | D)) is empty;

                then (( rng F) \ {(F . m)}) = {} by Th54;

                then

                 A10: ( rng F) = {(F . m)} by A9, ZFMISC_1: 58;



                 A11: for i, j st i in ( rng F) & j in ( rng F) & i < j holds ( min* (F " {i})) < ( min* (F " {j}))

                proof

                  let i, j such that

                   A12: i in ( rng F) and

                   A13: j in ( rng F) and

                   A14: i < j;

                  i = (F . m) by A10, A12, TARSKI:def 1;

                  hence thesis by A10, A13, A14, TARSKI:def 1;

                end;

                set P = ( id ( rng F));

                ( rng P) = ( rng F);

                then P is one-to-one onto by FUNCT_2:def 3;

                then

                reconsider P as Permutation of ( rng F);

                F is Function of ( dom F), ( rng F) by FUNCT_2: 1;

                then (P * F) = F by FUNCT_2: 17;

                hence thesis by A11;

              end;

                suppose

                 A15: ( rng (F | D)) is non empty;

                ( rng (F | D)) c= ( rng F) by RELAT_1: 70;

                then

                reconsider rFD = ( rng (F | D)) as non empty finite Subset of NAT by A7, A15, XBOOLE_1: 1;

                deffunc G( set) = (F . m);

                reconsider dFD = ( dom (F | D)) as Subset of NAT by XBOOLE_1: 1;

                reconsider FD = (F | D) as Function of dFD, rFD by FUNCT_2: 1;



                 A16: rFD is empty implies dFD is empty;

                reconsider rF = ( rng F) as non empty finite Subset of NAT by A7, A9, XBOOLE_1: 1;



                 A17: dFD c= N & rFD c= K;

                consider P be Permutation of ( rng FD), G be Function of dFD, rFD such that

                 A18: FD = (P * G) and

                 A19: ( rng FD) = ( rng G) and

                 A20: for i, j st i in ( rng G) & j in ( rng G) & i < j holds ( min* (G " {i})) < ( min* (G " {j})) by A5, A6, A9;



                 A21: for x st x in (N \ dFD) holds G(x) in K by A9;

                consider G2 be Function of N, K such that

                 A22: (G2 | dFD) = G & for x st x in (N \ dFD) holds (G2 . x) = G(x) from Sch2( A21, A17, A16);



                 A23: ( rng G2) c= ( rng F)

                proof

                  let Gx be object;

                  assume Gx in ( rng G2);

                  then

                  consider x be object such that

                   A24: x in ( dom G2) and

                   A25: (G2 . x) = Gx by FUNCT_1:def 3;

                  ( dom G2) = N by FUNCT_2:def 1;

                  then ((( dom G2) /\ dFD) \/ (N \ dFD)) = ( dom G2) by XBOOLE_1: 51;

                  then ( dom G) = (( dom G2) /\ dFD) & x in (( dom G2) /\ dFD) or x in (N \ dFD) by A22, A24, RELAT_1: 61, XBOOLE_0:def 3;

                  then (G . x) in ( rng FD) & (G . x) = (G2 . x) & ( rng FD) = (( rng F) \ {(F . m)}) or (G2 . x) = (F . m) & m in domF by A19, A22, Th54, FUNCT_1: 47, FUNCT_1:def 3, NAT_1:def 1;

                  hence thesis by A25, FUNCT_1:def 3, XBOOLE_0:def 5;

                end;



                 A26: ( rng FD) = (( rng F) \ {(F . m)}) by Th54;

                ( dom FD) = (( dom F) /\ (( dom F) \ (F " {(F . m)}))) by RELAT_1: 61;

                then

                 A27: dFD = (( dom F) \ (F " {(F . m)})) by XBOOLE_1: 28, XBOOLE_1: 36;



                 A28: (F " {(F . m)}) c= (G2 " {(F . m)})

                proof

                  let x be object such that

                   A29: x in (F " {(F . m)});

                   not x in (( dom F) \ (F " {(F . m)})) by A29, XBOOLE_0:def 5;

                  then x in (N \ dFD) by A27, A29, XBOOLE_0:def 5;

                  then (G2 . x) = (F . m) by A22;

                  then

                   A30: (G2 . x) in {(F . m)} by TARSKI:def 1;

                  x in N by A29;

                  then x in ( dom G2) by FUNCT_2:def 1;

                  hence thesis by A30, FUNCT_1:def 7;

                end;

                ( rng F) c= ( rng G2)

                proof

                  ( rng FD) = (( rng F) \ {(F . m)}) by Th54;

                  then

                   A31: ( rng F) = (( rng FD) \/ {(F . m)}) by A9, ZFMISC_1: 116;

                  let Fx be object such that

                   A32: Fx in ( rng F);

                  now

                    per cases by A32, A31, XBOOLE_0:def 3;

                      suppose

                       A33: Fx in ( rng FD);

                      ( rng (G2 | dFD)) c= ( rng G2) by RELAT_1: 70;

                      hence thesis by A19, A22, A33;

                    end;

                      suppose

                       A34: Fx in {(F . m)};



                       A35: m in ( dom F) by NAT_1:def 1;

                      then m in N;

                      then m in ( dom G2) by FUNCT_2:def 1;

                      then

                       A36: (G2 . m) in ( rng G2) by FUNCT_1:def 3;

                      (F . m) in {(F . m)} by TARSKI:def 1;

                      then m in (F " {(F . m)}) by A35, FUNCT_1:def 7;

                      then not m in (( dom F) \ (F " {(F . m)})) by XBOOLE_0:def 5;

                      then

                       A37: m in (N \ dFD) by A27, A35, XBOOLE_0:def 5;

                      Fx = (F . m) by A34, TARSKI:def 1;

                      hence thesis by A22, A37, A36;

                    end;

                  end;

                  hence thesis;

                end;

                then

                 A38: ( rng G2) = ( rng F) by A23;

                 not (F . m) in (( rng F) \ {(F . m)}) by ZFMISC_1: 56;

                then not (F . m) in ( rng FD) by Th54;

                then

                consider P2 be Function of (( rng FD) \/ {(F . m)}), (( rng FD) \/ {(F . m)}) such that

                 A39: (P2 | ( rng FD)) = P and

                 A40: (P2 . (F . m)) = (F . m) by Th57;

                 not (F . m) in (( rng F) \ {(F . m)}) by ZFMISC_1: 56;

                then

                 A41: P2 is one-to-one onto by A39, A40, A26, Th58;

                (( rng FD) \/ {(F . m)}) = ( rng F) by A9, A26, ZFMISC_1: 116;

                then

                reconsider P2 as Permutation of ( rng F) by A41;

                consider Orde be Function of rF, ( Segm ( card rF)) such that

                 A42: Orde is bijective and

                 A43: for n, k st n in ( dom Orde) & k in ( dom Orde) & n < k holds (Orde . n) < (Orde . k) by Th59;

                ( rng Orde) = ( card rF) by A42, FUNCT_2:def 3;

                then

                reconsider Orde9 = (Orde " ) as Function of ( card rF), rF by A42, FUNCT_2: 25;

                consider P1 be Permutation of rF such that

                 A44: for k st k in rF holds (k < (F . m) implies (P1 . k) = ((Orde " ) . ((Orde . k) + 1))) & (k = (F . m) implies (P1 . k) = ((Orde " ) . 0 )) & (k > (F . m) implies (P1 . k) = k) by A9, A42, A43, Lm5;

                ( dom G2) = N by FUNCT_2:def 1;

                then

                 A45: G2 is Function of N, rF by A38, FUNCT_2: 1;

                reconsider P21 = (P2 * (P1 " )) as Function of rF, rF;

                reconsider P21 as Permutation of rF;

                ( dom P1) = rF by FUNCT_2:def 1;

                then

                 A46: ((P1 " ) * P1) = ( id rF) by FUNCT_1: 39;

                ( rng (P1 * G2)) c= K by XBOOLE_1: 1;

                then

                reconsider PG = (P1 * G2) as Function of N, K by A45, FUNCT_2: 6;

                ( dom G2) = N by FUNCT_2:def 1;

                then G2 is Function of N, rF by A38, FUNCT_2: 1;

                then (( id rF) * G2) = G2 by FUNCT_2: 17;

                then

                 A47: ((P1 " ) * (P1 * G2)) = G2 by A46, RELAT_1: 36;

                (G2 " {(F . m)}) c= (F " {(F . m)})

                proof

                  let x be object such that

                   A48: x in (G2 " {(F . m)});



                   A49: x in (N \ dFD)

                  proof

                    assume not x in (N \ dFD);

                    then x in ( dom G2) & ( dom G2) = N & not x in N or x in dFD by A48, XBOOLE_0:def 5;

                    then

                     A50: x in ( dom G) by FUNCT_2:def 1;

                    then

                     A51: (G . x) in ( rng G) by FUNCT_1:def 3;



                     A52: ( rng FD) = (( rng F) \ {(F . m)}) by Th54;

                    (G . x) = (G2 . x) by A22, A50, FUNCT_1: 47;

                    then not (G2 . x) in {(F . m)} by A51, A52, XBOOLE_0:def 5;

                    hence thesis by A48, FUNCT_1:def 7;

                  end;

                  then

                   A53: not x in (( dom F) \ (F " {(F . m)})) by A27, XBOOLE_0:def 5;

                  ( dom F) = N by A9, FUNCT_2:def 1;

                  then x in ( dom F) by A49, XBOOLE_0:def 5;

                  hence thesis by A53, XBOOLE_0:def 5;

                end;

                then

                 A54: (G2 " {(F . m)}) = (F " {(F . m)}) by A28;



                 A55: for n st n in ( rng FD) holds (G " {n}) = (G2 " {n})

                proof

                  K is non empty;

                  then ( dom F) = N by FUNCT_2:def 1;

                  then

                   A56: dFD = (( dom G2) \ (G2 " {(F . m)})) by A27, A54, FUNCT_2:def 1;



                   A57: ( rng FD) = (( rng F) \ {(F . m)}) by Th54;

                  let n;

                  assume n in ( rng FD);

                  then not n in {(F . m)} by A57, XBOOLE_0:def 5;

                  then n <> (F . m) by TARSKI:def 1;

                  hence thesis by A22, A56, Th54;

                end;



                 A58: for i, j st i in ( rng PG) & j in ( rng PG) & i < j holds ( min* (PG " {i})) < ( min* (PG " {j}))

                proof



                   A59: for l st l in rF & l < (F . m) holds ((Orde . l) + 1) in ( rng Orde) & ((Orde . l) + 1) is Element of NAT & ((Orde . l) + 1) <= (Orde . (F . m)) & (Orde . (F . m)) is Element of NAT & ( dom Orde) = rF

                  proof



                     A60: ( dom Orde) = rF by FUNCT_2:def 1;



                     A61: (Orde . (F . m)) in ( card rF);



                     A62: (Orde . (F . m)) < ( card rF) by NAT_1: 44;

                    let l such that

                     A63: l in rF and

                     A64: l < (F . m);



                     A65: (Orde . l) < (Orde . (F . m)) by A9, A43, A63, A64, A60;

                    then ((Orde . l) + 1) <= (Orde . (F . m)) by NAT_1: 13;

                    then

                     A66: ((Orde . l) + 1) < ( card rF) by A62, XXREAL_0: 2;

                    ( card rF) = ( rng Orde) by A42, FUNCT_2:def 3;

                    hence thesis by A65, A61, A66, FUNCT_2:def 1, NAT_1: 13, NAT_1: 44;

                  end;



                   A67: for n, k st n in ( dom Orde) & k in ( dom Orde) & (Orde . n) < (Orde . k) holds n < k

                  proof

                    let n, k such that

                     A68: n in ( dom Orde) and

                     A69: k in ( dom Orde) and

                     A70: (Orde . n) < (Orde . k);

                    assume n >= k;

                    then n > k by A70, XXREAL_0: 1;

                    hence contradiction by A43, A68, A69, A70;

                  end;



                   A71: for n, k st n in ( rng Orde) & k in ( rng Orde) holds n < k implies (Orde9 . n) < (Orde9 . k)

                  proof

                    let n, k such that

                     A72: n in ( rng Orde) and

                     A73: k in ( rng Orde);



                     A74: n = (Orde . (Orde9 . n)) by A42, A72, FUNCT_1: 35;



                     A75: ( dom Orde) = ( rng Orde9) by A42, FUNCT_1: 33;



                     A76: k = (Orde . (Orde9 . k)) by A42, A73, FUNCT_1: 35;

                    assume

                     A77: n < k;



                     A78: ( rng Orde) = ( dom Orde9) by A42, FUNCT_1: 33;

                    then

                     A79: (Orde9 . n) in ( dom Orde) by A72, A75, FUNCT_1:def 3;

                    (Orde9 . k) in ( dom Orde) by A73, A78, A75, FUNCT_1:def 3;

                    hence thesis by A67, A77, A74, A76, A79;

                  end;

                  ( rng FD) = (( rng F) \ {(F . m)}) by Th54;

                  then

                   A80: (( rng FD) \/ {(F . m)}) = ( rng G2) by A9, A38, ZFMISC_1: 116;

                  let i, j such that

                   A81: i in ( rng PG) and

                   A82: j in ( rng PG) and

                   A83: i < j;

                  consider i1 be set such that

                   A84: i1 in ( dom P1) and

                   A85: i1 in ( rng G2) and

                   A86: (P1 " {i}) = {i1} and

                   A87: (G2 " {i1}) = (PG " {i}) by A81, Th61;

                  consider j1 be set such that

                   A88: j1 in ( dom P1) and

                   A89: j1 in ( rng G2) and

                   A90: (P1 " {j}) = {j1} and

                   A91: (G2 " {j1}) = (PG " {j}) by A82, Th61;

                  ( dom P1) = rF by FUNCT_2:def 1;

                  then

                  reconsider i1, j1 as Element of NAT by A84, A88;



                   A92: i1 in (P1 " {i}) by A86, TARSKI:def 1;

                  then (P1 . i1) in {i} by FUNCT_1:def 7;

                  then

                   A93: (P1 . i1) = i by TARSKI:def 1;



                   A94: j1 in (P1 " {j}) by A90, TARSKI:def 1;

                  then

                   A95: (P1 . j1) in {j} by FUNCT_1:def 7;

                  then

                   A96: (P1 . j1) = j by TARSKI:def 1;



                   A97: ( dom Orde) = rF by FUNCT_2:def 1;

                  now

                    per cases by XXREAL_0: 1;

                      suppose

                       A98: i1 < (F . m) & j1 < (F . m);



                       A99: i1 in ( rng FD) or i1 in {(F . m)} by A85, A80, XBOOLE_0:def 3;

                      then

                       A100: (G " {i1}) = (PG " {i}) by A55, A87, A98, TARSKI:def 1;



                       A101: j1 in ( rng FD) or j1 in {(F . m)} by A89, A80, XBOOLE_0:def 3;

                      i1 < j1

                      proof

                        assume i1 >= j1;

                        then i1 > j1 by A83, A93, A96, XXREAL_0: 1;

                        then (Orde . i1) > (Orde . j1) by A43, A92, A94, A97;

                        then

                         A102: ((Orde . i1) + 1) > ((Orde . j1) + 1) by XREAL_1: 8;



                         A103: ((Orde . i1) + 1) in ( rng Orde) by A84, A59, A98;



                         A104: (Orde9 . ((Orde . j1) + 1)) = j by A44, A94, A96, A98;



                         A105: ((Orde . j1) + 1) in ( rng Orde) by A88, A59, A98;

                        (Orde9 . ((Orde . i1) + 1)) = i by A44, A92, A93, A98;

                        hence contradiction by A83, A71, A102, A103, A105, A104;

                      end;

                      then ( min* (G " {i1})) < ( min* (G " {j1})) by A19, A20, A98, A99, A101, TARSKI:def 1;

                      hence thesis by A55, A91, A98, A101, A100, TARSKI:def 1;

                    end;

                      suppose

                       A106: i1 = (F . m) & j1 <> (F . m);

                      consider x be object such that

                       A107: x in ( dom G2) and

                       A108: (G2 . x) = j1 by A89, FUNCT_1:def 3;

                      (G2 . x) in {j1} by A108, TARSKI:def 1;

                      then (PG " {j}) is non empty Subset of NAT by A91, A107, FUNCT_1:def 7, XBOOLE_1: 1;

                      then

                       A109: ( min* (PG " {j})) in (PG " {j}) by NAT_1:def 1;

                      j1 in ( rng FD) or j1 in {(F . m)} by A89, A80, XBOOLE_0:def 3;

                      then

                       A110: (G " {j1}) = (PG " {j}) by A55, A91, A106, TARSKI:def 1;

                      then ( min* (PG " {j})) in ( dom F) by A27, A109, XBOOLE_0:def 5;

                      then

                       A111: m <= ( min* (PG " {j})) by NAT_1:def 1;



                       A112: m in domF by NAT_1:def 1;

                      (F . m) in {(F . m)} by TARSKI:def 1;

                      then

                       A113: m in (F " {(F . m)}) by A112, FUNCT_1:def 7;

                      then m <> ( min* (PG " {j})) by A27, A110, A109, XBOOLE_0:def 5;

                      then

                       A114: m < ( min* (PG " {j})) by A111, XXREAL_0: 1;

                      (PG " {i}) is Subset of NAT by XBOOLE_1: 1;

                      then ( min* (PG " {i})) <= m by A28, A87, A106, A113, NAT_1:def 1;

                      hence thesis by A114, XXREAL_0: 2;

                    end;

                      suppose

                       A115: i1 < (F . m) & j1 = (F . m);

                      ( card rF) = ( rng Orde) by A42, FUNCT_2:def 3;

                      then

                       A116: 0 in ( rng Orde) by NAT_1: 44;

                      ((Orde . i1) + 1) in ( rng Orde) by A84, A59, A115;

                      then

                       A117: (Orde9 . ((Orde . i1) + 1)) > (Orde9 . 0 ) by A71, A116;



                       A118: (P1 . j1) = (Orde9 . 0 ) by A44, A94, A115;

                      (Orde9 . ((Orde . i1) + 1)) = i by A44, A92, A93, A115;

                      hence thesis by A83, A95, A117, A118, TARSKI:def 1;

                    end;

                      suppose i1 = (F . m) & j1 = (F . m);

                      hence thesis by A83, A95, A93, TARSKI:def 1;

                    end;

                      suppose

                       A119: i1 > (F . m) & j1 > (F . m);



                       A120: i1 in ( rng FD) or i1 in {(F . m)} by A85, A80, XBOOLE_0:def 3;

                      then

                       A121: (G " {i1}) = (PG " {i}) by A55, A87, A119, TARSKI:def 1;



                       A122: (P1 . j1) = j1 by A44, A88, A119;



                       A123: j1 in ( rng FD) or j1 in {(F . m)} by A89, A80, XBOOLE_0:def 3;

                      (P1 . i1) = i1 by A44, A84, A119;

                      then ( min* (G " {i1})) < ( min* (G " {j1})) by A19, A20, A83, A93, A96, A119, A122, A120, A123, TARSKI:def 1;

                      hence thesis by A55, A91, A119, A123, A121, TARSKI:def 1;

                    end;

                      suppose

                       A124: i1 > (F . m) & j1 = (F . m);



                       A125: ( dom Orde) = rF by FUNCT_2:def 1;

                      ( rng (Orde " )) = ( dom Orde) by A42, FUNCT_1: 33;

                      then

                      consider x be object such that

                       A126: x in ( dom Orde9) and

                       A127: (Orde9 . x) = i1 by A84, A125, FUNCT_1:def 3;



                       A128: x in ( card rF) by A126;

                      ( card rF) is Subset of NAT by Th8;

                      then

                      reconsider x as Element of NAT by A128;

                      (P1 . i1) = i1 by A44, A84, A124;

                      then

                       A129: (Orde9 . x) < (Orde9 . 0 ) by A44, A83, A88, A93, A96, A124, A127;



                       A130: ( card rF) = ( rng Orde) by A42, FUNCT_2:def 3;

                      then 0 in ( rng Orde) by NAT_1: 44;

                      then x <= 0 by A71, A126, A130, A129;

                      hence thesis by A129;

                    end;

                      suppose

                       A131: i1 < (F . m) & j1 > (F . m);



                       A132: i1 in ( rng FD) or i1 in {(F . m)} by A85, A80, XBOOLE_0:def 3;

                      then

                       A133: (G " {i1}) = (PG " {i}) by A55, A87, A131, TARSKI:def 1;



                       A134: j1 in ( rng FD) or j1 in {(F . m)} by A89, A80, XBOOLE_0:def 3;

                      i1 < j1 by A131, XXREAL_0: 2;

                      then ( min* (G " {i1})) < ( min* (G " {j1})) by A19, A20, A131, A132, A134, TARSKI:def 1;

                      hence thesis by A55, A91, A131, A134, A133, TARSKI:def 1;

                    end;

                      suppose

                       A135: i1 > (F . m) & j1 < (F . m);

                      then ( dom Orde) = rF by A88, A59;

                      then

                       A136: (Orde . (F . m)) in ( rng Orde) by A9, FUNCT_1:def 3;

                      ((Orde . j1) + 1) <= (Orde . (F . m)) by A88, A59, A135;

                      then

                       A137: ((Orde . j1) + 1) < (Orde . (F . m)) or ((Orde . j1) + 1) = (Orde . (F . m)) by XXREAL_0: 1;

                      (F . m) in ( dom Orde) by A9, A88, A59, A135;

                      then

                       A138: (Orde9 . (Orde . (F . m))) = (F . m) by A42, FUNCT_1: 34;



                       A139: (P1 . i1) = i1 by A44, A84, A135;



                       A140: (Orde9 . ((Orde . j1) + 1)) = (P1 . j1) by A44, A88, A135;

                      ((Orde . j1) + 1) in ( rng Orde) by A88, A59, A135;

                      then (P1 . j1) <= (F . m) by A71, A137, A136, A138, A140;

                      hence thesis by A83, A93, A96, A135, A139, XXREAL_0: 2;

                    end;

                  end;

                  hence thesis;

                end;

                K is non empty;

                then

                 A141: ( dom F) = N by FUNCT_2:def 1;



                 A142: for x be object st x in ( dom F) holds (F . x) = (P2 . (G2 . x))

                proof

                  let x be object such that

                   A143: x in ( dom F);

                  now

                    per cases by A143, XBOOLE_0:def 5;

                      suppose

                       A144: x in (N \ dFD);

                      then

                       A145: not x in (( dom F) \ (F " {(F . m)})) by A27, XBOOLE_0:def 5;

                      x in ( dom F) by A141, A144, XBOOLE_0:def 5;

                      then x in (F " {(F . m)}) by A145, XBOOLE_0:def 5;

                      then

                       A146: (F . x) in {(F . m)} by FUNCT_1:def 7;

                      (P2 . (G2 . x)) = (F . m) by A22, A40, A144;

                      hence thesis by A146, TARSKI:def 1;

                    end;

                      suppose

                       A147: x in dFD;

                      then

                       A148: (F . x) = (FD . x) by FUNCT_1: 47;



                       A149: (FD . x) = (P . (G . x)) by A18, A147, FUNCT_1: 12;



                       A150: ( dom P) = ( rng FD) by FUNCT_2:def 1;



                       A151: x in ( dom G) by A147, FUNCT_2:def 1;

                      then

                       A152: (G . x) in ( rng FD) by A19, FUNCT_1:def 3;

                      (G . x) = (G2 . x) by A22, A151, FUNCT_1: 47;

                      hence thesis by A39, A148, A149, A152, A150, FUNCT_1: 47;

                    end;

                  end;

                  hence thesis;

                end;



                 A153: ( dom G2) = N by FUNCT_2:def 1;

                for x be object holds x in ( dom F) iff x in ( dom G2) & (G2 . x) in ( dom P2)

                proof

                  let x be object;

                  thus x in ( dom F) implies x in ( dom G2) & (G2 . x) in ( dom P2)

                  proof

                    assume

                     A154: x in ( dom F);

                    then ( dom P2) = ( rng F) by A153, FUNCT_2:def 1;

                    hence thesis by A38, A153, A154, FUNCT_1:def 3;

                  end;

                  thus thesis by A141;

                end;

                then F = (P2 * G2) by A142, FUNCT_1: 10;

                then

                 A155: F = (P21 * PG) by A47, RELAT_1: 36;

                ( rng P1) = rF by FUNCT_2:def 3;

                then ( rng (P1 * G2)) = rF by A38, A45, FUNCT_2: 14;

                hence thesis by A155, A58;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;



       A156: for F be Function st ( rng F) is finite holds P[F] from Sch9( A1, A4);

      let F be Function of Ne, Ke;

      assume ( rng F) is finite;

      then

      consider P be Permutation of ( rng F), G be Function of Ne, Ke such that

       A157: F = (P * G) and

       A158: ( rng F) = ( rng G) and

       A159: for i, j st i in ( rng G) & j in ( rng G) & i < j holds ( min* (G " {i})) < ( min* (G " {j})) by A156;

      G is 'increasing by A159;

      hence thesis by A157, A158;

    end;

    theorem :: STIRL2_1:64



     Th64: for F be Function of Ne, Ke st ( rng F) is finite holds for I1,I2 be Function of Ne, Me, P1,P2 be Function st P1 is one-to-one & P2 is one-to-one & ( rng I1) = ( rng I2) & ( rng I1) = ( dom P1) & ( dom P1) = ( dom P2) & F = (P1 * I1) & F = (P2 * I2) & I1 is 'increasing & I2 is 'increasing holds P1 = P2 & I1 = I2

    proof

      defpred Q[ set, Function] means $1 = ($2 . ( min* ( dom $2)));

      defpred P[ set] means for Ne,Ke,Me be Subset of NAT holds for F be Function of Ne, Ke st F = $1 holds for I1,I2 be Function of Ne, Me, P1,P2 be Function st P1 is one-to-one & P2 is one-to-one & ( rng I1) = ( rng I2) & ( rng I1) = ( dom P1) & ( dom P1) = ( dom P2) & F = (P1 * I1) & F = (P2 * I2) & I1 is 'increasing & I2 is 'increasing holds P1 = P2 & I1 = I2;



       A1: P[ {} ]

      proof

        let Ne,Ke,Me be Subset of NAT ;

        let F be Function of Ne, Ke such that

         A2: F = {} ;

        let I1,I2 be Function of Ne, Me, P1,P2 be Function such that P1 is one-to-one and P2 is one-to-one and

         A3: ( rng I1) = ( rng I2) and

         A4: ( rng I1) = ( dom P1) and

         A5: ( dom P1) = ( dom P2) and

         A6: F = (P1 * I1) and F = (P2 * I2) and I1 is 'increasing and I2 is 'increasing;

        ( dom I1) = {} by A2, A4, A6, RELAT_1: 27;

        then

         A7: I1 = {} ;

        ( rng P1) = {} by A2, A4, A6, RELAT_1: 28, RELAT_1: 38;

        then P1 = {} ;

        hence thesis by A3, A5, A7;

      end;



       A8: for F be Function st for x st x in ( rng F) & Q[x, F] holds P[(F | (( dom F) \ (F " {x})))] holds P[F]

      proof

        let F9 be Function such that

         A9: for x st x in ( rng F9) & Q[x, F9] holds P[(F9 | (( dom F9) \ (F9 " {x})))];

        now

          per cases ;

            suppose F9 = {} ;

            hence thesis by A1;

          end;

            suppose

             A10: F9 <> {} ;

            let Ne,Ke,Me be Subset of NAT ;

            let F be Function of Ne, Ke such that

             A11: F = F9;

            Ke is non empty by A10, A11;

            then

            reconsider domF = ( dom F) as non empty Subset of NAT by A10, A11, FUNCT_2:def 1;

            set m = ( min* ( dom F));

            let I1,I2 be Function of Ne, Me, P1,P2 be Function such that

             A12: P1 is one-to-one and

             A13: P2 is one-to-one and

             A14: ( rng I1) = ( rng I2) and

             A15: ( rng I1) = ( dom P1) and

             A16: ( dom P1) = ( dom P2) and

             A17: F = (P1 * I1) and

             A18: F = (P2 * I2) and

             A19: I1 is 'increasing and

             A20: I2 is 'increasing;

            ( dom I1) = ( dom F) by A15, A17, RELAT_1: 27;

            then

             A21: ( min* ( rng I1)) = (I1 . m) by A19, Th62;

            reconsider I = (( rng I1) \ {(I1 . m)}) as Subset of NAT by XBOOLE_1: 1;

            reconsider D = (( dom F) \ (F " {(F . m)})) as Subset of NAT by XBOOLE_1: 1;



             A22: for I be Function of Ne, Me, P be Function st P is one-to-one & ( rng I) = ( dom P) & F = (P * I) & I is 'increasing holds ( dom (I | D)) = D & ( rng (I | D)) = (( rng I) \ {(I . m)}) & ( dom (P | (( rng I) \ {(I . m)}))) = (( rng I) \ {(I . m)}) & (F | D) = ((P | (( rng I) \ {(I . m)})) * (I | D)) & (P | (( rng I) \ {(I . m)})) is one-to-one & for M be Subset of NAT st M = (( rng I) \ {(I . m)}) holds for I1 be Function of D, M st I1 = (I | D) holds I1 is 'increasing

            proof



               A23: (F . m) in {(F . m)} by TARSKI:def 1;

              let I be Function of Ne, Me, P be Function such that

               A24: P is one-to-one and

               A25: ( rng I) = ( dom P) and

               A26: F = (P * I) and

               A27: I is 'increasing;



               A28: (( dom P) /\ (( rng I) \ {(I . m)})) = (( rng I) \ {(I . m)}) by A25, XBOOLE_1: 28, XBOOLE_1: 36;

              m in domF by NAT_1:def 1;

              then (F . m) in ( rng F) by FUNCT_1:def 3;

              then

              consider x such that x in ( dom P) and x in ( rng I) and (P " {(F . m)}) = {x} and

               A29: (I " {x}) = (F " {(F . m)}) by A24, A26, Th61;



               A30: ( dom (P | (( rng I) \ {(I . m)}))) = (( dom P) /\ (( rng I) \ {(I . m)})) by RELAT_1: 61;



               A31: ( dom F) = ( dom I) by A25, A26, RELAT_1: 27;

              then

               A32: (( dom I) /\ D) = D by XBOOLE_1: 28, XBOOLE_1: 36;

              m in domF by NAT_1:def 1;

              then m in (I " {x}) by A29, A23, FUNCT_1:def 7;

              then (I . m) in {x} by FUNCT_1:def 7;

              then

               A33: (I . m) = x by TARSKI:def 1;



               A34: for M be Subset of NAT st M = (( rng I) \ {(I . m)}) holds for I1 be Function of D, M st I1 = (I | D) holds I1 is 'increasing

              proof

                let M be Subset of NAT such that M = (( rng I) \ {(I . m)});

                let I1 be Function of D, M such that

                 A35: I1 = (I | D);



                 A36: ( rng I1) = (( rng I) \ {(I . m)}) by A29, A33, A31, A35, Th54;

                let l, n such that

                 A37: l in ( rng I1) and

                 A38: n in ( rng I1) and

                 A39: l < n;



                 A40: n in ( rng I) by A38, A36, ZFMISC_1: 56;

                n <> (I . m) by A38, A36, ZFMISC_1: 56;

                then

                 A41: (I1 " {n}) = (I " {n}) by A29, A33, A31, A35, Th54;

                l <> (I . m) by A37, A36, ZFMISC_1: 56;

                then

                 A42: (I1 " {l}) = (I " {l}) by A29, A33, A31, A35, Th54;

                l in ( rng I) by A37, A36, ZFMISC_1: 56;

                hence thesis by A27, A39, A40, A42, A41;

              end;

              set rI = (( rng I) \ {(I . m)});



               A43: ( dom (I | D)) = (( dom I) /\ D) by RELAT_1: 61;



               A44: ( rng (I | D)) = (( rng I) \ {(I . m)}) by A29, A33, A31, Th54;



               A45: for x be object st x in ( dom (F | D)) holds ((F | D) . x) = ((P | rI) . ((I | D) . x))

              proof

                let x be object such that

                 A46: x in ( dom (F | D));



                 A47: x in (( dom F) /\ D) by A46, RELAT_1: 61;

                then

                 A48: x in ( dom F) by XBOOLE_0:def 4;

                ((I | D) . x) in ( dom (P | rI)) by A31, A43, A30, A28, A44, A47, FUNCT_1:def 3;

                then

                 A49: ((P | rI) . ((I | D) . x)) = (P . ((I | D) . x)) by FUNCT_1: 47;



                 A50: ((F | D) . x) = (F . x) by A46, FUNCT_1: 47;

                (I . x) = ((I | D) . x) by A31, A43, A47, FUNCT_1: 47;

                hence thesis by A26, A48, A49, A50, FUNCT_1: 12;

              end;

              (( dom F) /\ D) = D by XBOOLE_1: 28, XBOOLE_1: 36;

              then ( dom (F | D)) = D by RELAT_1: 61;

              then for x be object holds x in ( dom (F | D)) iff x in ( dom (I | D)) & ((I | D) . x) in ( dom (P | rI)) by A43, A32, A30, A28, A44, FUNCT_1:def 3;

              hence thesis by A24, A29, A33, A31, A32, A28, A45, A34, Th54, FUNCT_1: 10, FUNCT_1: 52, RELAT_1: 61;

            end;

            then

             A51: (P1 | I) is one-to-one by A12, A15, A17, A19;

            ( dom I2) = ( dom F) by A14, A15, A16, A18, RELAT_1: 27;

            then

             A52: ( min* ( rng I2)) = (I2 . m) by A20, Th62;

            then

             A53: (P2 | I) is one-to-one by A13, A14, A15, A16, A18, A20, A22, A21;



             A54: ( dom (I2 | D)) = D by A13, A14, A15, A16, A18, A20, A22;



             A55: ( dom (I1 | D)) = D by A12, A15, A17, A19, A22;



             A56: ( rng (I1 | D)) = I by A12, A15, A17, A19, A22;

            ( rng (I2 | D)) = I by A13, A14, A15, A16, A18, A20, A22, A21, A52;

            then

            reconsider I1D = (I1 | D), I2D = (I2 | D) as Function of D, I by A55, A54, A56, FUNCT_2: 1;



             A57: I2D is 'increasing by A13, A14, A15, A16, A18, A20, A22, A21, A52;



             A58: ( rng I1D) = I by A12, A15, A17, A19, A22;

            then

             A59: ( rng I1D) = ( dom (P1 | I)) by A12, A15, A17, A19, A22;

            reconsider rFD = ( rng (F | D)) as Subset of NAT by XBOOLE_1: 1;

            (( dom F) /\ D) = D by XBOOLE_1: 28, XBOOLE_1: 36;

            then ( dom (F | D)) = D by RELAT_1: 61;

            then

            reconsider FD = (F | D) as Function of D, rFD by FUNCT_2: 1;



             A60: FD = ((P1 | I) * I1D) by A12, A15, A17, A19, A22;



             A61: FD = ((P2 | I) * I2D) by A13, A14, A15, A16, A18, A20, A22, A21, A52;

            m in domF by NAT_1:def 1;

            then

             A62: (F . m) in ( rng F) by FUNCT_1:def 3;

            ( dom (P1 | I)) = I by A12, A15, A17, A19, A22;

            then

             A63: ( dom (P1 | I)) = ( dom (P2 | I)) by A13, A14, A15, A16, A18, A20, A22, A21, A52;



             A64: I1D is 'increasing by A12, A15, A17, A19, A22;



             A65: ( rng I1D) = ( rng I2D) by A13, A14, A15, A16, A18, A20, A22, A21, A52, A58;

            for x be object st x in ( dom P1) holds (P1 . x) = (P2 . x)

            proof



               A66: m in domF by NAT_1:def 1;

              ( dom I1) = ( dom F) by A15, A17, RELAT_1: 27;

              then (I1 . m) in ( rng I1) by A66, FUNCT_1:def 3;

              then

               A67: ( dom P1) = (I \/ {(I1 . m)}) by A15, ZFMISC_1: 116;

              let x be object such that

               A68: x in ( dom P1);

              now

                per cases by A68, A67, XBOOLE_0:def 3;

                  suppose

                   A69: x in I;

                  (( dom P1) /\ I) = I by A15, XBOOLE_1: 28, XBOOLE_1: 36;

                  then x in ( dom (P1 | I)) by A69, RELAT_1: 61;

                  then

                   A70: ((P1 | I) . x) = (P1 . x) by FUNCT_1: 47;

                  (( dom P2) /\ I) = I by A15, A16, XBOOLE_1: 28, XBOOLE_1: 36;

                  then x in ( dom (P2 | I)) by A69, RELAT_1: 61;

                  then ((P2 | I) . x) = (P2 . x) by FUNCT_1: 47;

                  hence thesis by A9, A11, A62, A51, A53, A65, A59, A63, A60, A61, A64, A57, A70;

                end;

                  suppose

                   A71: x in {(I1 . m)};



                   A72: m in domF by NAT_1:def 1;



                   A73: x = (I1 . m) by A71, TARSKI:def 1;

                  then (F . m) = (P1 . x) by A17, A72, FUNCT_1: 12;

                  hence thesis by A14, A18, A21, A52, A73, A72, FUNCT_1: 12;

                end;

              end;

              hence thesis;

            end;

            then

             A74: P1 = P2 by A16;

            I2 is Function of ( dom I2), ( rng I2) by FUNCT_2: 1;

            then

             A75: I2 = (( id ( rng I2)) * I2) by FUNCT_2: 17;

            I1 is Function of ( dom I1), ( rng I1) by FUNCT_2: 1;

            then

             A76: I1 = (( id ( rng I1)) * I1) by FUNCT_2: 17;

            ((P1 " ) * P1) = ( id ( dom P1)) by A12, FUNCT_1: 39;

            then

             A77: I1 = ((P1 " ) * (P1 * I1)) by A15, A76, RELAT_1: 36;

            ((P2 " ) * P2) = ( id ( dom P2)) by A13, FUNCT_1: 39;

            hence P1 = P2 & I1 = I2 by A14, A15, A17, A18, A74, A75, A77, RELAT_1: 36;

          end;

        end;

        hence thesis;

      end;

      for F be Function st ( rng F) is finite holds P[F] from Sch9( A1, A8);

      hence thesis;

    end;

    theorem :: STIRL2_1:65

    for F be Function of Ne, Ke st ( rng F) is finite holds for I1,I2 be Function of Ne, Ke, P1,P2 be Permutation of ( rng F) st F = (P1 * I1) & F = (P2 * I2) & ( rng F) = ( rng I1) & ( rng F) = ( rng I2) & I1 is 'increasing & I2 is 'increasing holds P1 = P2 & I1 = I2

    proof

      let F be Function of Ne, Ke such that

       A1: ( rng F) is finite;

      let I1,I2 be Function of Ne, Ke, P1,P2 be Permutation of ( rng F) such that

       A2: F = (P1 * I1) and

       A3: F = (P2 * I2) and

       A4: ( rng F) = ( rng I1) and

       A5: ( rng F) = ( rng I2) and

       A6: I1 is 'increasing and

       A7: I2 is 'increasing;



       A8: ( rng F) = {} implies ( rng F) = {} ;

      then

       A9: ( dom P2) = ( rng F) by FUNCT_2:def 1;

      ( dom P1) = ( rng F) by A8, FUNCT_2:def 1;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A9, Th64;

    end;

    ::$Notion-Name

    theorem :: STIRL2_1:66

    for D be non empty set, F be XFinSequence of D st (for i st i in ( dom F) holds (F . i) is finite) & (for i, j st i in ( dom F) & j in ( dom F) & i <> j holds (F . i) misses (F . j)) holds ex CardF be XFinSequence of NAT st ( dom CardF) = ( dom F) & (for i st i in ( dom CardF) holds (CardF . i) = ( card (F . i))) & ( card ( union ( rng F))) = ( Sum CardF) by Lm2;