card_fin.miz

    begin

    reserve x,x1,x2,y,z,X9 for set,

X,Y for finite set,

n,k,m for Nat,

f for Function;

    ::$Canceled

    theorem :: CARD_FIN:2



     Th1: for X, Y, x, y st (Y = {} implies X = {} ) & not x in X holds ( card ( Funcs (X,Y))) = ( card { F where F be Function of (X \/ {x}), (Y \/ {y}) : ( rng (F | X)) c= Y & (F . x) = y })

    proof

      defpred P[ set, set, set] means 1 = 1;

      let X, Y, x, y;

      assume

       A1: Y = {} implies X = {} ;

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



       A2: 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 F1 = { f where f be Function of X, Y : P[f, X, Y] };

      assume

       A3: not x in X;

      set F3 = { F where F be Function of (X \/ {x}), (Y \/ {y}) : ( rng (F | X)) c= Y & (F . x) = y };



       A4: ( Funcs (X,Y)) c= F1

      proof

        let F be object;

        assume F in ( Funcs (X,Y));

        then F is Function of X, Y by FUNCT_2: 66;

        hence thesis;

      end;



       A5: F2 c= F3

      proof

        let F be object;

        assume F in F2;

        then ex f be Function of (X \/ {x}), (Y \/ {y}) st f = F & P[f, (X \/ {x}), (Y \/ {y})] & ( rng (f | X)) c= Y & (f . x) = y;

        hence thesis;

      end;



       A6: Y is empty implies X is empty by A1;



       A7: ( card F1) = ( card F2) from STIRL2_1:sch 4( A6, A3, A2);



       A8: F3 c= F2

      proof

        let F be object;

        assume F in F3;

        then ex f be Function of (X \/ {x}), (Y \/ {y}) st f = F & ( rng (f | X)) c= Y & (f . x) = y;

        hence thesis;

      end;

      F1 c= ( Funcs (X,Y))

      proof

        let F be object;

        assume F in F1;

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

        hence thesis by A1, FUNCT_2: 8;

      end;

      then ( Funcs (X,Y)) = F1 by A4;

      hence thesis by A5, A8, A7, XBOOLE_0:def 10;

    end;

    theorem :: CARD_FIN:3



     Th2: for X, Y, x, y st not x in X & y in Y holds ( card ( Funcs (X,Y))) = ( card { F where F be Function of (X \/ {x}), Y : (F . x) = y })

    proof

      let X, Y, x, y such that

       A1: not x in X and

       A2: y in Y;

      set F2 = { F where F be Function of (X \/ {x}), Y : (F . x) = y };

      set F1 = { F where F be Function of (X \/ {x}), (Y \/ {y}) : ( rng (F | X)) c= Y & (F . x) = y };

       {y} c= Y by A2, ZFMISC_1: 31;

      then

       A3: Y = (Y \/ {y}) by XBOOLE_1: 12;



       A4: F2 c= F1

      proof

        let f be object;

        assume f in F2;

        then

        consider F be Function of (X \/ {x}), Y such that

         A5: f = F & (F . x) = y;

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

        hence thesis by A3, A5;

      end;

      F1 c= F2

      proof

        let f be object;

        assume f in F1;

        then ex F be Function of (X \/ {x}), (Y \/ {y}) st f = F & ( rng (F | X)) c= Y & (F . x) = y;

        hence thesis by A3;

      end;

      then F1 = F2 by A4;

      hence thesis by A1, A2, Th1;

    end;

    theorem :: CARD_FIN:4



     Th3: (Y = {} implies X = {} ) implies ( card ( Funcs (X,Y))) = (( card Y) |^ ( card X))

    proof

      assume

       A1: Y = {} implies X = {} ;

      per cases ;

        suppose

         A2: Y is empty;

        then ( card ( Funcs (X,Y))) = 1 by A1, CARD_1: 30, FUNCT_2: 127;

        hence thesis by A1, A2, NEWTON: 4;

      end;

        suppose

         A3: Y is non empty;

        defpred P[ Nat] means for X, Y st Y is non empty & ( card X) = $1 holds ( card ( Funcs (X,Y))) = (( card Y) |^ ( card X));



         A4: for n st P[n] holds P[(n + 1)]

        proof

          defpred Q[ set] means 1 = 1;

          let n such that

           A5: P[n];

          let X, Y such that

           A6: Y is non empty and

           A7: ( card X) = (n + 1);

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

          reconsider cY = (( card Y) |^ nn) as Element of NAT ;

          (( card Y),Y) are_equipotent by CARD_1:def 2;

          then

          consider f be Function such that

           A8: f is one-to-one and

           A9: ( dom f) = ( card Y) and

           A10: ( rng f) = Y by WELLORD2:def 4;

          reconsider f as Function of ( card Y), Y by A9, A10, FUNCT_2: 1;

          consider x be object such that

           A11: x in X by A7, CARD_1: 27, XBOOLE_0:def 1;

          reconsider x as set by TARSKI: 1;



           A12: x in X by A11;



           A13: f is onto one-to-one by A8, A10, FUNCT_2:def 3;

          consider F be XFinSequence of NAT such that

           A14: ( dom F) = ( card Y) and

           A15: ( card { g where g be Function of X, Y : Q[g] }) = ( Sum F) and

           A16: for k st k in ( dom F) holds (F . k) = ( card { g where g be Function of X, Y : Q[g] & (g . x) = (f . k) }) from STIRL2_1:sch 6( A13, A6, A12);



           A17: for k be Nat st k in ( dom F) holds (F . k) = cY

          proof

            set Xx = (X \ {x});

            let k be Nat such that

             A18: k in ( dom F);



             A19: (f . k) in ( rng f) by A9, A14, A18, FUNCT_1:def 3;

            set F3 = { g where g be Function of X, Y : Q[g] & (g . x) = (f . k) };

            set F2 = { g where g be Function of (Xx \/ {x}), Y : (g . x) = (f . k) };



             A20: F3 c= F2

            proof

              let G be object;

              assume G in F3;

              then

               A21: ex g be Function of X, Y st g = G & Q[g] & (g . x) = (f . k);

              (Xx \/ {x}) = X by A12, ZFMISC_1: 116;

              hence thesis by A21;

            end;

            F2 c= F3

            proof

              let G be object;

              assume G in F2;

              then

               A22: ex g be Function of (Xx \/ {x}), Y st g = G & (g . x) = (f . k);

              (Xx \/ {x}) = X by A12, ZFMISC_1: 116;

              hence thesis by A22;

            end;

            then

             A23: F2 = F3 by A20;

            ( card Xx) = n by A7, A12, STIRL2_1: 55;

            then

             A24: ( card ( Funcs (Xx,Y))) = cY by A5, A19;

            x in {x} by TARSKI:def 1;

            then not x in Xx by XBOOLE_0:def 5;

            then ( card ( Funcs (Xx,Y))) = ( card F2) by A19, Th2;

            hence thesis by A16, A18, A23, A24;

          end;

          then for k be Nat st k in ( dom F) holds (F . k) >= cY;

          then

           A25: ( Sum F) >= (( len F) * (( card Y) |^ n)) by AFINSQ_2: 60;

          set F1 = { g where g be Function of X, Y : Q[g] };



           A26: ( Funcs (X,Y)) c= F1

          proof

            let G be object;

            assume G in ( Funcs (X,Y));

            then G is Function of X, Y by FUNCT_2: 66;

            hence thesis;

          end;

          F1 c= ( Funcs (X,Y))

          proof

            let G be object;

            assume G in F1;

            then ex g be Function of X, Y st g = G & Q[g];

            hence thesis by A6, FUNCT_2: 8;

          end;

          then

           A27: ( Funcs (X,Y)) = F1 by A26;

          for k be Nat st k in ( dom F) holds (F . k) <= cY by A17;

          then ( Sum F) <= (( len F) * (( card Y) |^ n)) by AFINSQ_2: 59;

          then ( Sum F) = (( card Y) * (( card Y) |^ n)) by A14, A25, XXREAL_0: 1;

          hence thesis by A7, A15, A27, NEWTON: 6;

        end;



         A28: P[ 0 ]

        proof

          let X, Y such that Y is non empty and

           A29: ( card X) = 0 ;

          X is empty by A29;

          then ( Funcs (X,Y)) = { {} } by FUNCT_5: 57;

          then ( card ( Funcs (X,Y))) = 1 by CARD_1: 30;

          hence thesis by A29, NEWTON: 4;

        end;

        for n holds P[n] from NAT_1:sch 2( A28, A4);

        hence thesis by A3;

      end;

    end;

    theorem :: CARD_FIN:5



     Th4: for X, Y, x, y st (Y is empty implies X is empty) & not x in X & not y in Y holds ( card { F where F be Function of X, Y : F is one-to-one }) = ( card { F where F be Function of (X \/ {x}), (Y \/ {y}) : F is one-to-one & (F . x) = y })

    proof

      let X, Y, x, y such that

       A1: Y is empty implies X is empty and

       A2: not x in X and

       A3: not y in Y;

      defpred P[ Function, set, set] means $1 is one-to-one & ( rng ($1 | X)) c= Y;



       A4: 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]

      proof

        let f be Function of (X \/ {x}), (Y \/ {y}) such that

         A5: (f . x) = y;

        thus P[f, (X \/ {x}), (Y \/ {y})] implies P[(f | X), X, Y] by FUNCT_1: 52;

        thus P[(f | X), X, Y] implies P[f, (X \/ {x}), (Y \/ {y})]

        proof

          ((X \/ {x}) /\ X) = X & ( dom f) = (X \/ {x}) by FUNCT_2:def 1, XBOOLE_1: 21;

          then

           A6: ( dom (f | X)) = X by RELAT_1: 61;

          assume that

           A7: (f | X) is one-to-one and

           A8: ( rng ((f | X) | X)) c= Y;

          ( rng (f | X)) c= Y by A8;

          then (f | X) is Function of X, Y by A6, FUNCT_2: 2;

          hence thesis by A1, A3, A5, A7, A8, STIRL2_1: 58;

        end;

      end;

      set F3 = { F where F be Function of (X \/ {x}), (Y \/ {y}) : F is one-to-one & (F . x) = y };



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

      proof

        let z be object;

        assume z in F3;

        then

        consider F be Function of (X \/ {x}), (Y \/ {y}) such that

         A10: z = F and

         A11: F is one-to-one & (F . x) = y;

        ( rng (F | X)) c= Y

        proof



           A12: ( dom F) = (X \/ {x}) by FUNCT_2:def 1;

          x in {x} by TARSKI:def 1;

          then

           A13: x in ( dom F) by A12, XBOOLE_0:def 3;

          assume not ( rng (F | X)) c= Y;

          then

          consider fz be object such that

           A14: fz in ( rng (F | X)) and

           A15: not fz in Y;

          consider z be object such that

           A16: z in ( dom (F | X)) and

           A17: fz = ((F | X) . z) by A14, FUNCT_1:def 3;



           A18: z in ( dom F) by A16, RELAT_1: 57;



           A19: fz in Y or fz in {y} by A14, XBOOLE_0:def 3;



           A20: z in X by A16;

          (F . z) = ((F | X) . z) by A16, FUNCT_1: 47;

          then y = (F . z) by A15, A17, A19, TARSKI:def 1;

          hence thesis by A2, A11, A13, A20, A18;

        end;

        hence thesis by A10, A11;

      end;



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

      proof

        let z be object;

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

        then ex f be Function of (X \/ {x}), (Y \/ {y}) st z = f & P[f, (X \/ {x}), (Y \/ {y})] & ( rng (f | X)) c= Y & (f . x) = y;

        hence thesis;

      end;

      set F2 = { f where f be Function of X, Y : f is one-to-one & ( rng (f | X)) c= Y };

      set F1 = { F where F be Function of X, Y : F is one-to-one };



       A22: F1 c= F2

      proof

        let z be object;

        assume z in F1;

        then

        consider F be Function of X, Y such that

         A23: z = F & F is one-to-one;

        ( rng (F | X)) c= ( rng F);

        hence thesis by A23;

      end;



       A24: not x in X by A2;



       A25: ( 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 }) from STIRL2_1:sch 4( A1, A24, A4);

      F2 c= F1

      proof

        let z be object;

        assume z in F2;

        then ex f be Function of X, Y st z = f & f is one-to-one & ( rng (f | X)) c= Y;

        hence thesis;

      end;

      then F2 = F1 by A22;

      hence thesis by A9, A21, A25, XBOOLE_0:def 10;

    end;

    theorem :: CARD_FIN:6

    ((n ! ) / ((n -' k) ! )) is Element of NAT

    proof

      ((n ! ) / ((n -' k) ! )) is integer by IRRAT_1: 36, NAT_D: 35;

      hence thesis by INT_1: 3;

    end;

    theorem :: CARD_FIN:7



     Th6: ( card X) <= ( card Y) implies ( card { F where F be Function of X, Y : F is one-to-one }) = ((( card Y) ! ) / ((( card Y) -' ( card X)) ! ))

    proof

      defpred P[ Nat] means for X, Y st ( card Y) = $1 & ( card X) <= ( card Y) holds ( card { F where F be Function of X, Y : F is one-to-one }) = ((( card Y) ! ) / ((( card Y) -' ( card X)) ! ));



       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A2: P[n];

        let X, Y such that

         A3: ( card Y) = (n + 1) and

         A4: ( card X) <= ( card Y);

        per cases ;

          suppose

           A5: X is empty;

          set F1 = { F where F be Function of X, Y : F is one-to-one };



           A6: F1 c= { {} }

          proof

            let x be object;

            assume x in F1;

            then ex F be Function of X, Y st x = F & F is one-to-one;

            then x = {} by A5;

            hence thesis by TARSKI:def 1;

          end;



           A7: ( rng {} ) c= Y;

          (( card Y) - ( card X)) = ( card Y) by A5;

          then

           A8: ((( card Y) -' ( card X)) ! ) = (( card Y) ! ) by XREAL_0:def 2;



           A9: ((( card Y) ! ) / ((( card Y) -' ( card X)) ! )) = 1 by A8, XCMPLX_1: 60;

          ( dom {} ) = X by A5;

          then {} is Function of X, Y by A7, FUNCT_2: 2;

          then {} in F1;

          then F1 = { {} } by A6, ZFMISC_1: 33;

          hence thesis by A9, CARD_1: 30;

        end;

          suppose X is non empty;

          then

          consider x be object such that

           A10: x in X;

          reconsider x as set by TARSKI: 1;



           A11: x in X by A10;

          defpred F[ Function] means $1 is one-to-one;

          (( card Y),Y) are_equipotent by CARD_1:def 2;

          then

          consider f be Function such that

           A12: f is one-to-one and

           A13: ( dom f) = ( card Y) and

           A14: ( rng f) = Y by WELLORD2:def 4;

          reconsider f as Function of ( card Y), Y by A13, A14, FUNCT_2: 1;



           A15: Y is non empty by A3;



           A16: f is onto one-to-one by A12, A14, FUNCT_2:def 3;

          consider F be XFinSequence of NAT such that

           A17: ( dom F) = ( card Y) and

           A18: ( card { g where g be Function of X, Y : F[g] }) = ( Sum F) and

           A19: for k st k in ( dom F) holds (F . k) = ( card { g where g be Function of X, Y : F[g] & (g . x) = (f . k) }) from STIRL2_1:sch 6( A16, A15, A11);



           A20: for k be Nat st k in ( dom F) holds (F . k) = ((n ! ) / ((( card Y) -' ( card X)) ! ))

          proof

            ( card X) > 0 by A11;

            then

            reconsider cX1 = (( card X) - 1) as Element of NAT by NAT_1: 20;

            set Xx = (X \ {x});

            x in {x} by TARSKI:def 1;

            then

             A21: not x in Xx by XBOOLE_0:def 5;



             A22: X = (Xx \/ {x}) by A11, ZFMISC_1: 116;



             A23: ((cX1 + 1) - 1) <= ((n + 1) - 1) by A3, A4, XREAL_1: 9;

            then

             A24: (n - cX1) >= (cX1 - cX1) by XREAL_1: 9;

            let k be Nat such that

             A25: k in ( dom F);



             A26: (f . k) in Y by A13, A14, A17, A25, FUNCT_1:def 3;

            set Yy = (Y \ {(f . k)});



             A27: Y = (Yy \/ {(f . k)}) by A26, ZFMISC_1: 116;

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

            then

             A28: not (f . k) in Yy by XBOOLE_0:def 5;

            (cX1 + 1) <= (n + 1) by A3, A4;

            then

             A29: ( card Xx) = cX1 by A11, STIRL2_1: 55;



             A30: ( card Yy) = n by A3, A26, STIRL2_1: 55;

            then

             A31: Yy is empty implies Xx is empty by A23, A29;



             A32: ( card { g where g be Function of Xx, Yy : g is one-to-one }) = ((n ! ) / ((( card Yy) -' ( card Xx)) ! )) by A2, A23, A29, A30;

            (( card Y) - ( card X)) >= (( card X) - ( card X)) by A4, XREAL_1: 9;



            then (( card Y) -' ( card X)) = (((( card Yy) + 1) - 1) - ((( card Xx) + 1) - 1)) by A3, A29, A30, XREAL_0:def 2

            .= (( card Yy) -' ( card Xx)) by A29, A30, A24, XREAL_0:def 2;

            then ( card { g where g be Function of X, Y : g is one-to-one & (g . x) = (f . k) }) = ((n ! ) / ((( card Y) -' ( card X)) ! )) by A32, A27, A22, A28, A21, A31, Th4;

            hence thesis by A19, A25;

          end;

          then for k be Nat st k in ( dom F) holds (F . k) >= ((n ! ) / ((( card Y) -' ( card X)) ! ));

          then

           A33: ( Sum F) >= (( len F) * ((n ! ) / ((( card Y) -' ( card X)) ! ))) by AFINSQ_2: 60;

          for k be Nat st k in ( dom F) holds (F . k) <= ((n ! ) / ((( card Y) -' ( card X)) ! )) by A20;

          then ( Sum F) <= (( len F) * ((n ! ) / ((( card Y) -' ( card X)) ! ))) by AFINSQ_2: 59;



          then ( Sum F) = ((n + 1) * ((n ! ) / ((( card Y) -' ( card X)) ! ))) by A3, A17, A33, XXREAL_0: 1

          .= (((n + 1) * (n ! )) / ((( card Y) -' ( card X)) ! )) by XCMPLX_1: 74

          .= ((( card Y) ! ) / ((( card Y) -' ( card X)) ! )) by A3, NEWTON: 15;

          hence thesis by A18;

        end;

      end;



       A34: P[ 0 ]

      proof

        let X, Y such that

         A35: ( card Y) = 0 and

         A36: ( card X) <= ( card Y);

        (( card Y) - ( card X)) = 0 by A35, A36;

        then

         A37: ((( card Y) -' ( card X)) ! ) = 1 by NEWTON: 12, XREAL_0:def 2;

        set F1 = { F where F be Function of X, Y : F is one-to-one };



         A38: F1 c= { {} }

        proof

          let x be object;

          assume x in F1;

          then

           A39: ex F be Function of X, Y st x = F & F is one-to-one;

          Y = {} by A35;

          then x = {} by A39;

          hence thesis by TARSKI:def 1;

        end;

        ( dom {} ) = X & ( rng {} ) = Y by A35, A36;

        then {} is Function of X, Y by FUNCT_2: 1;

        then {} in F1;

        then F1 = { {} } by A38, ZFMISC_1: 33;

        hence thesis by A35, A37, CARD_1: 30, NEWTON: 12;

      end;

      for n holds P[n] from NAT_1:sch 2( A34, A1);

      hence thesis;

    end;

    theorem :: CARD_FIN:8



     Th7: ( card { F where F be Function of X, X : F is Permutation of X }) = (( card X) ! )

    proof

      set F1 = { F where F be Function of X, X : F is one-to-one };

      set F2 = { F where F be Function of X, X : F is Permutation of X };



       A1: F1 c= F2

      proof

        let x be object;

        assume x in F1;

        then

        consider F be Function of X, X such that

         A2: x = F and

         A3: F is one-to-one;

        ( card X) = ( card X);

        then F is onto by A3, FINSEQ_4: 63;

        hence thesis by A2, A3;

      end;

      ((( card X) -' ( card X)) ! ) = 1 by NEWTON: 12, XREAL_1: 232;

      then

       A4: ((( card X) ! ) / ((( card X) -' ( card X)) ! )) = (( card X) ! );

      F2 c= F1

      proof

        let x be object;

        assume x in F2;

        then ex F be Function of X, X st x = F & F is Permutation of X;

        hence thesis;

      end;

      then F1 = F2 by A1;

      hence thesis by A4, Th6;

    end;

    definition

      let X, k;

      let x1,x2 be object;

      :: CARD_FIN:def1

      func Choose (X,k,x1,x2) -> Subset of ( Funcs (X, {x1, x2})) means

      : Def1: x in it iff ex f be Function of X, {x1, x2} st f = x & ( card (f " {x1})) = k;

      existence

      proof

        defpred P[ object] means ex f be Function of X, {x1, x2} st $1 = f & ( card (f " {x1})) = k;

        consider F be set such that

         A1: for x be object holds x in F iff x in ( bool [:X, {x1, x2}:]) & P[x] from XBOOLE_0:sch 1;

        F c= ( Funcs (X, {x1, x2}))

        proof

          let x be object;

          assume x in F;

          then ex f be Function of X, {x1, x2} st x = f & ( card (f " {x1})) = k by A1;

          hence thesis by FUNCT_2: 8;

        end;

        then

        reconsider F as Subset of ( Funcs (X, {x1, x2}));

        take F;

        let x;

        thus x in F implies ex f be Function of X, {x1, x2} st x = f & ( card (f " {x1})) = k by A1;

        given f be Function of X, {x1, x2} such that

         A2: x = f & ( card (f " {x1})) = k;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let F1,F2 be Subset of ( Funcs (X, {x1, x2})) such that

         A3: x in F1 iff ex f be Function of X, {x1, x2} st x = f & ( card (f " {x1})) = k and

         A4: x in F2 iff ex f be Function of X, {x1, x2} st x = f & ( card (f " {x1})) = k;

        for x be object holds x in F1 iff x in F2

        proof

          let x be object;

          x in F1 iff ex f be Function of X, {x1, x2} st x = f & ( card (f " {x1})) = k by A3;

          hence thesis by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: CARD_FIN:9

    ( card X) <> k implies ( Choose (X,k,x1,x1)) is empty

    proof

      assume

       A1: ( card X) <> k;

      assume ( Choose (X,k,x1,x1)) is non empty;

      then

      consider y be object such that

       A2: y in ( Choose (X,k,x1,x1));

      consider f be Function of X, {x1, x1} such that f = y and

       A3: ( card (f " {x1})) = k by A2, Def1;

      per cases ;

        suppose

         A4: ( rng f) is empty;



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

        ( dom f) = {} by A4, RELAT_1: 42;

        hence thesis by A1, A3, A5;

      end;

        suppose

         A6: ( rng f) is non empty;

         {x1, x1} = {x1} by ENUMSET1: 29;

        then ( rng f) = {x1} by A6, ZFMISC_1: 33;

        then (f " {x1}) = ( dom f) by RELAT_1: 134;

        hence thesis by A1, A3, FUNCT_2:def 1;

      end;

    end;

    theorem :: CARD_FIN:10



     Th9: for x1,x2 be object holds ( card X) < k implies ( Choose (X,k,x1,x2)) is empty

    proof

      let x1,x2 be object;

      assume

       A1: ( card X) < k;

      assume ( Choose (X,k,x1,x2)) is non empty;

      then

      consider z be object such that

       A2: z in ( Choose (X,k,x1,x2));

      ex f be Function of X, {x1, x2} st f = z & ( card (f " {x1})) = k by A2, Def1;

      hence thesis by A1, NAT_1: 43;

    end;

    theorem :: CARD_FIN:11



     Th10: for x1,x2 be object holds x1 <> x2 implies ( card ( Choose (X, 0 ,x1,x2))) = 1

    proof

      let x1,x2 be object;

      assume

       A1: x1 <> x2;

      per cases ;

        suppose

         A2: X is empty;

        ( dom {} ) = X by A2;

        then

        reconsider Empty = {} as Function of X, {x1, x2} by XBOOLE_1: 2;



         A3: ( Choose (X, 0 ,x1,x2)) c= {Empty}

        proof

          let z be object;

          assume z in ( Choose (X, 0 ,x1,x2));

          then

          consider f be Function of X, {x1, x2} such that

           A4: z = f and ( card (f " {x1})) = 0 by Def1;

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

          then f = Empty;

          hence thesis by A4, TARSKI:def 1;

        end;

        (Empty " {x1}) = {} & ( card {} ) = 0 ;

        then Empty in ( Choose (X, 0 ,x1,x2)) by Def1;

        then ( Choose (X, 0 ,x1,x2)) = {Empty} by A3, ZFMISC_1: 33;

        hence thesis by CARD_1: 30;

      end;

        suppose

         A5: X is non empty;

        then

        consider f be Function such that

         A6: ( dom f) = X and

         A7: ( rng f) = {x2} by FUNCT_1: 5;

        ( rng f) c= {x1, x2} by A7, ZFMISC_1: 36;

        then

         A8: f is Function of X, {x1, x2} by A6, FUNCT_2: 2;



         A9: ( Choose (X, 0 ,x1,x2)) c= {f}

        proof

          let z be object;

          assume z in ( Choose (X, 0 ,x1,x2));

          then

          consider g be Function of X, {x1, x2} such that

           A10: z = g and

           A11: ( card (g " {x1})) = 0 by Def1;

          (g " {x1}) = {} by A11;

          then not x1 in ( rng g) by FUNCT_1: 72;

          then ( not ( rng g) = {x1}) & not ( rng g) = {x1, x2} by TARSKI:def 1, TARSKI:def 2;

          then ( dom g) = X & ( rng g) = {x2} by A5, FUNCT_2:def 1, ZFMISC_1: 36;

          then g = f by A6, A7, FUNCT_1: 7;

          hence thesis by A10, TARSKI:def 1;

        end;

         not x1 in ( rng f) by A1, A7, TARSKI:def 1;

        then

         A12: (f " {x1}) = {} by FUNCT_1: 72;

        ( card {} ) = 0 ;

        then f in ( Choose (X, 0 ,x1,x2)) by A12, A8, Def1;

        then ( Choose (X, 0 ,x1,x2)) = {f} by A9, ZFMISC_1: 33;

        hence thesis by CARD_1: 30;

      end;

    end;

    theorem :: CARD_FIN:12



     Th11: for x1,x2 be object holds ( card ( Choose (X,( card X),x1,x2))) = 1

    proof

      let x1,x2 be object;

      per cases ;

        suppose

         A1: X is empty;

        ( dom {} ) = X by A1;

        then

        reconsider Empty = {} as Function of X, {x1, x2} by XBOOLE_1: 2;



         A2: ( Choose (X,( card X),x1,x2)) c= {Empty}

        proof

          let z be object;

          assume z in ( Choose (X,( card X),x1,x2));

          then

          consider f be Function of X, {x1, x2} such that

           A3: z = f and ( card (f " {x1})) = ( card X) by Def1;

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

          then f = Empty;

          hence thesis by A3, TARSKI:def 1;

        end;

        (Empty " {x1}) = {} ;

        then Empty in ( Choose (X,( card X),x1,x2)) by A1, Def1;

        then ( Choose (X,( card X),x1,x2)) = {Empty} by A2, ZFMISC_1: 33;

        hence thesis by CARD_1: 30;

      end;

        suppose

         A4: X is non empty;

        then

        consider f be Function such that

         A5: ( dom f) = X and

         A6: ( rng f) = {x1} by FUNCT_1: 5;

        ( rng f) c= {x1, x2} by A6, ZFMISC_1: 36;

        then

         A7: f is Function of X, {x1, x2} by A5, FUNCT_2: 2;



         A8: ( Choose (X,( card X),x1,x2)) c= {f}

        proof

          let z be object;

          assume z in ( Choose (X,( card X),x1,x2));

          then

          consider g be Function of X, {x1, x2} such that

           A9: z = g and

           A10: ( card (g " {x1})) = ( card X) by Def1;

           A11:

          now

            per cases ;

              suppose x1 = x2;

              then {x1, x2} = {x1} by ENUMSET1: 29;

              hence ( rng g) = {x1} by A4, ZFMISC_1: 33;

            end;

              suppose

               A12: x1 <> x2;

              (g " {x2}) = {}

              proof

                assume (g " {x2}) <> {} ;

                then

                consider z be object such that

                 A13: z in (g " {x2}) by XBOOLE_0:def 1;

                (g . z) in {x2} by A13, FUNCT_1:def 7;

                then

                 A14: (g . z) = x2 by TARSKI:def 1;

                (g " {x1}) = X by A10, CARD_2: 102;

                then (g . z) in {x1} by A13, FUNCT_1:def 7;

                hence thesis by A12, A14, TARSKI:def 1;

              end;

              then not x2 in ( rng g) by FUNCT_1: 72;

              then ( not ( rng g) = {x2}) & not ( rng g) = {x1, x2} by TARSKI:def 1, TARSKI:def 2;

              hence ( rng g) = {x1} by A4, ZFMISC_1: 36;

            end;

          end;

          ( dom g) = X by FUNCT_2:def 1;

          then g = f by A5, A6, A11, FUNCT_1: 7;

          hence thesis by A9, TARSKI:def 1;

        end;

        ( card (f " {x1})) = ( card X) by A5, A6, RELAT_1: 134;

        then f in ( Choose (X,( card X),x1,x2)) by A7, Def1;

        then ( Choose (X,( card X),x1,x2)) = {f} by A8, ZFMISC_1: 33;

        hence thesis by CARD_1: 30;

      end;

    end;

    theorem :: CARD_FIN:13



     Th12: for z,x,y be object holds not z in X implies ( card ( Choose (X,k,x,y))) = ( card { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = x })

    proof

      let z,x,y be object;

      set F1 = { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = x };

      defpred P[ set, set, set] means for f be Function st f = $1 holds ( card ((f | X) " {x})) = k;



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

      proof

        let f be Function of (X \/ {z}), ( {x, y} \/ {x}) such that (f . z) = x;

        (f | X) = ((f | X) | X);

        hence thesis;

      end;

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

      set F2 = { f where f be Function of X, {x, y} : P[f, X, {x, y}] };

      assume

       A2: not z in X;



       A3: F3 c= F1

      proof

        ( {x} \/ {x, y}) = {x, x, y} by ENUMSET1: 2;

        then

         A4: ( {x, y} \/ {x}) = {x, y} by ENUMSET1: 30;

        z in {z} by TARSKI:def 1;

        then

         A5: z in (X \/ {z}) by XBOOLE_0:def 3;

        let x1 be object;

        assume x1 in F3;

        then

        consider f be Function of (X \/ {z}), ( {x, y} \/ {x}) such that

         A6: x1 = f and

         A7: P[f, (X \/ {z}), ( {x, y} \/ {x})] and ( rng (f | X)) c= {x, y} and

         A8: (f . z) = x;

        ( dom f) = (X \/ {z}) & ((X \/ {z}) \ {z}) = X by A2, FUNCT_2:def 1, ZFMISC_1: 117;

        then

         A9: ( {z} \/ ((f | X) " {x})) = (f " {x}) by A8, A5, AFINSQ_2: 66;

         not z in (( dom f) /\ X) by A2, XBOOLE_0:def 4;

        then not z in ( dom (f | X)) by RELAT_1: 61;

        then

         A10: not z in ((f | X) " {x}) by FUNCT_1:def 7;

        ( card ((f | X) " {x})) = k by A7;

        then ( card (f " {x})) = (k + 1) by A9, A10, CARD_2: 41;

        hence thesis by A6, A8, A4;

      end;



       A11: F2 c= ( Choose (X,k,x,y))

      proof

        let x1 be object;

        assume x1 in F2;

        then

        consider f be Function of X, {x, y} such that

         A12: x1 = f and

         A13: P[f, X, {x, y}];

        (f | X) = f;

        then ( card (f " {x})) = k by A13;

        hence thesis by A12, Def1;

      end;



       A14: ( Choose (X,k,x,y)) c= F2

      proof

        let x1 be object;

        assume x1 in ( Choose (X,k,x,y));

        then

        consider f be Function of X, {x, y} such that

         A15: x1 = f and

         A16: ( card (f " {x})) = k by Def1;

         P[f, X, {x, y}] by A16;

        hence thesis by A15;

      end;



       A17: {x, y} is empty implies X is empty;



       A18: ( card F2) = ( card F3) from STIRL2_1:sch 4( A17, A2, A1);

      F1 c= F3

      proof

        z in {z} by TARSKI:def 1;

        then

         A19: z in (X \/ {z}) by XBOOLE_0:def 3;

        let x1 be object;

        assume x1 in F1;

        then

        consider f be Function of (X \/ {z}), {x, y} such that

         A20: x1 = f and

         A21: ( card (f " {x})) = (k + 1) and

         A22: (f . z) = x;

         not z in (( dom f) /\ X) by A2, XBOOLE_0:def 4;

        then not z in ( dom (f | X)) by RELAT_1: 61;

        then

         A23: not z in ((f | X) " {x}) by FUNCT_1:def 7;

        ( dom f) = (X \/ {z}) & ((X \/ {z}) \ {z}) = X by A2, FUNCT_2:def 1, ZFMISC_1: 117;

        then (((f | X) " {x}) \/ {z}) = (f " {x}) by A22, A19, AFINSQ_2: 66;

        then (( card ((f | X) " {x})) + 1) = (k + 1) by A21, A23, CARD_2: 41;

        then

         A24: P[f, (X \/ {z}), ( {x, y} \/ {x})];

        ( {x} \/ {x, y}) = {x, x, y} by ENUMSET1: 2;

        then ( rng (f | X)) c= {x, y} & f is Function of (X \/ {z}), ( {x, y} \/ {x}) by ENUMSET1: 30;

        hence thesis by A20, A22, A24;

      end;

      then F1 = F3 by A3;

      hence thesis by A11, A14, A18, XBOOLE_0:def 10;

    end;

    theorem :: CARD_FIN:14



     Th13: for z,x,y be object holds not z in X & x <> y implies ( card ( Choose (X,k,x,y))) = ( card { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = k & (f . z) = y })

    proof

      let z,x,y be object;

      assume that

       A1: not z in X and

       A2: x <> y;

      defpred P[ set, set, set] means for f be Function st f = $1 holds ( card (f " {x})) = k;



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

      proof

        let f be Function of (X \/ {z}), ( {x, y} \/ {y}) such that

         A4: (f . z) = y;

        ((X \/ {z}) \ {z}) = X & ( dom f) = (X \/ {z}) by A1, FUNCT_2:def 1, ZFMISC_1: 117;

        then ((f | X) " {x}) = (f " {x}) by A2, A4, AFINSQ_2: 67;

        hence thesis;

      end;

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

      set F1 = { f where f be Function of X, {x, y} : P[f, X, {x, y}] };



       A5: {x, y} is empty implies X is empty;



       A6: ( card F1) = ( card F2) from STIRL2_1:sch 4( A5, A1, A3);

      set F3 = { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = k & (f . z) = y };



       A7: F2 c= F3

      proof

        let x1 be object;

        assume x1 in F2;

        then

        consider f be Function of (X \/ {z}), ( {x, y} \/ {y}) such that

         A8: x1 = f and

         A9: P[f, (X \/ {z}), ( {x, y} \/ {y})] and ( rng (f | X)) c= {x, y} and

         A10: (f . z) = y;

        ( {x, y} \/ {y}) = {y, y, x} by ENUMSET1: 2;

        then

         A11: f is Function of (X \/ {z}), {x, y} by ENUMSET1: 30;

        ( card (f " {x})) = k by A9;

        hence thesis by A8, A10, A11;

      end;



       A12: F3 c= F2

      proof

        let x1 be object;

        assume x1 in F3;

        then

        consider f be Function of (X \/ {z}), {x, y} such that

         A13: f = x1 and

         A14: ( card (f " {x})) = k and

         A15: (f . z) = y;

        ( {x, y} \/ {y}) = {y, y, x} by ENUMSET1: 2;

        then

         A16: ( rng (f | X)) c= {x, y} & f is Function of (X \/ {z}), ( {x, y} \/ {y}) by ENUMSET1: 30;

         P[f, (X \/ {z}), ( {x, y} \/ {y})] by A14;

        hence thesis by A13, A15, A16;

      end;



       A17: ( Choose (X,k,x,y)) c= F1

      proof

        let x1 be object;

        assume x1 in ( Choose (X,k,x,y));

        then

        consider f be Function of X, {x, y} such that

         A18: x1 = f and

         A19: ( card (f " {x})) = k by Def1;

         P[f, X, {x, y}] by A19;

        hence thesis by A18;

      end;

      F1 c= ( Choose (X,k,x,y))

      proof

        let x1 be object;

        assume x1 in F1;

        then

        consider f be Function of X, {x, y} such that

         A20: x1 = f and

         A21: P[f, X, {x, y}];

        ( card (f " {x})) = k by A21;

        hence thesis by A20, Def1;

      end;

      then ( Choose (X,k,x,y)) = F1 by A17;

      hence thesis by A7, A12, A6, XBOOLE_0:def 10;

    end;



     Lm1: for z,x,y be object holds x <> y implies ({ f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = x } \/ { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = y }) = ( Choose ((X \/ {z}),(k + 1),x,y)) & { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = x } misses { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = y }

    proof

      let z,x,y be object;

      set F1 = { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = x };

      set F2 = { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = y };

      assume

       A1: x <> y;



       A2: F1 misses F2

      proof

        assume F1 meets F2;

        then (F1 /\ F2) <> {} ;

        then

        consider x1 be object such that

         A3: x1 in (F1 /\ F2) by XBOOLE_0:def 1;

        x1 in F2 by A3, XBOOLE_0:def 4;

        then

         A4: ex f2 be Function of (X \/ {z}), {x, y} st x1 = f2 & ( card (f2 " {x})) = (k + 1) & (f2 . z) = y;

        x1 in F1 by A3, XBOOLE_0:def 4;

        then ex f1 be Function of (X \/ {z}), {x, y} st x1 = f1 & ( card (f1 " {x})) = (k + 1) & (f1 . z) = x;

        hence thesis by A1, A4;

      end;



       A5: F2 c= ( Choose ((X \/ {z}),(k + 1),x,y))

      proof

        let x1 be object;

        assume x1 in F2;

        then ex f be Function of (X \/ {z}), {x, y} st x1 = f & ( card (f " {x})) = (k + 1) & (f . z) = y;

        hence thesis by Def1;

      end;



       A6: ( Choose ((X \/ {z}),(k + 1),x,y)) c= (F1 \/ F2)

      proof

        let x1 be object;

        assume x1 in ( Choose ((X \/ {z}),(k + 1),x,y));

        then

        consider f be Function of (X \/ {z}), {x, y} such that

         A7: f = x1 & ( card (f " {x})) = (k + 1) by Def1;

        z in {z} by TARSKI:def 1;

        then

         A8: z in (X \/ {z}) by XBOOLE_0:def 3;

        ( dom f) = (X \/ {z}) by FUNCT_2:def 1;

        then (f . z) in ( rng f) by A8, FUNCT_1:def 3;

        then (f . z) = x or (f . z) = y by TARSKI:def 2;

        then x1 in F1 or x1 in F2 by A7;

        hence thesis by XBOOLE_0:def 3;

      end;

      F1 c= ( Choose ((X \/ {z}),(k + 1),x,y))

      proof

        let x1 be object;

        assume x1 in F1;

        then ex f be Function of (X \/ {z}), {x, y} st x1 = f & ( card (f " {x})) = (k + 1) & (f . z) = x;

        hence thesis by Def1;

      end;

      then (F1 \/ F2) c= ( Choose ((X \/ {z}),(k + 1),x,y)) by A5, XBOOLE_1: 8;

      hence thesis by A6, A2;

    end;

    theorem :: CARD_FIN:15



     Th14: for z,x,y be object holds x <> y & not z in X implies ( card ( Choose ((X \/ {z}),(k + 1),x,y))) = (( card ( Choose (X,(k + 1),x,y))) + ( card ( Choose (X,k,x,y))))

    proof

      let z,x,y be object;

      assume that

       A1: x <> y and

       A2: not z in X;

      set F2 = { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = y };

      set F1 = { f where f be Function of (X \/ {z}), {x, y} : ( card (f " {x})) = (k + 1) & (f . z) = x };



       A3: (F1 \/ F2) = ( Choose ((X \/ {z}),(k + 1),x,y)) by A1, Lm1;

      F1 c= (F1 \/ F2) & F2 c= (F1 \/ F2) by XBOOLE_1: 7;

      then

      reconsider F1, F2 as finite set by A3;



       A4: ( card F1) = ( card ( Choose (X,k,x,y))) by A2, Th12;

      ( card (F1 \/ F2)) = (( card F1) + ( card F2)) & ( card F2) = ( card ( Choose (X,(k + 1),x,y))) by A1, A2, Lm1, Th13, CARD_2: 40;

      hence thesis by A1, A4, Lm1;

    end;

    ::$Notion-Name

    theorem :: CARD_FIN:16



     Th15: for x,y be object holds x <> y implies ( card ( Choose (X,k,x,y))) = (( card X) choose k)

    proof

      let x,y be object;

      defpred P[ Nat] means for k, X st (k + ( card X)) <= $1 holds ( card ( Choose (X,k,x,y))) = (( card X) choose k);

      assume

       A1: x <> y;



       A2: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A3: P[n];

        let k, X such that

         A4: (k + ( card X)) <= (n + 1);

        per cases by A4, XXREAL_0: 1;

          suppose (k + ( card X)) < (n + 1);

          then (k + ( card X)) <= n by NAT_1: 13;

          hence thesis by A3;

        end;

          suppose

           A5: (k + ( card X)) = (n + 1);

          per cases ;

            suppose

             A6: k = 0 & ( card X) >= 0 ;

            then ( card ( Choose (X,k,x,y))) = 1 by A1, Th10;

            hence thesis by A6, NEWTON: 19;

          end;

            suppose

             A7: k > 0 & ( card X) = 0 ;

            then ( Choose (X,k,x,y)) is empty by Th9;

            hence thesis by A7, NEWTON:def 3;

          end;

            suppose

             A8: k > 0 & ( card X) > 0 ;

            then

            reconsider cXz = (( card X) - 1) as Element of NAT by NAT_1: 20;

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

            consider z be object such that

             A9: z in X by A8, CARD_1: 27, XBOOLE_0:def 1;

            set Xz = (X \ {z});

            z in {z} by TARSKI:def 1;

            then

             A10: not z in Xz by XBOOLE_0:def 5;

            (Xz \/ {z}) = X by A9, ZFMISC_1: 116;

            then

             A11: ( card ( Choose (X,(k1 + 1),x,y))) = (( card ( Choose (Xz,(k1 + 1),x,y))) + ( card ( Choose (Xz,k1,x,y)))) by A1, A10, Th14;

            ( card X) = (cXz + 1);

            then

             A12: ( card Xz) = cXz by A9, STIRL2_1: 55;

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

            then

             A13: ( card Xz) < ( card X) by A9, STIRL2_1: 55;

            then (k + ( card Xz)) < (n + 1) by A5, XREAL_1: 8;

            then (k + ( card Xz)) <= n by NAT_1: 13;

            then

             A14: ( card ( Choose (Xz,(k1 + 1),x,y))) = (( card Xz) choose (k1 + 1)) by A3;

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

            then (k1 + ( card Xz)) < (n + 1) by A5, A13, XREAL_1: 8;

            then (k1 + ( card Xz)) <= n by NAT_1: 13;

            then

             A15: ( card ( Choose (Xz,k1,x,y))) = (( card Xz) choose k1) by A3;

            ( card X) = (cXz + 1);

            hence thesis by A14, A15, A11, A12, NEWTON: 22;

          end;

        end;

      end;



       A16: P[ 0 ]

      proof

        let k, X;



         A17: ( 0 choose 0 ) = 1 by NEWTON: 19;

        assume (k + ( card X)) <= 0 ;

        then (k + ( card X)) = 0 & ( card X) = 0 ;

        hence thesis by A1, Th10, A17;

      end;

      for n holds P[n] from NAT_1:sch 2( A16, A2);

      then P[(k + ( card X))];

      hence thesis;

    end;

    theorem :: CARD_FIN:17



     Th16: for x,y be object holds x <> y implies ((Y --> y) +* (X --> x)) in ( Choose ((X \/ Y),( card X),x,y))

    proof

      let x,y be object;

      set F = ((Y --> y) +* (X --> x));

      ( dom (Y --> y)) = Y & ( dom (X --> x)) = X;

      then

       A1: ( dom F) = (X \/ Y) by FUNCT_4:def 1;

       {y} c= {x, y} by ZFMISC_1: 7;

      then

       A2: ( rng (Y --> y)) c= {x, y};

       {x} c= {x, y} by ZFMISC_1: 7;

      then ( rng (X --> x)) c= {x, y};

      then ( rng F) c= (( rng (X --> x)) \/ ( rng (Y --> y))) & (( rng (X --> x)) \/ ( rng (Y --> y))) c= {x, y} by A2, FUNCT_4: 17, XBOOLE_1: 8;

      then

      reconsider F as Function of (X \/ Y), {x, y} by A1, FUNCT_2: 2, XBOOLE_1: 1;

      assume

       A3: x <> y;



       A4: (F " {x}) c= X

      proof

        let z be object such that

         A5: z in (F " {x});



         A6: z in X or z in Y by A5, XBOOLE_0:def 3;

        (F . z) in {x} by A5, FUNCT_1:def 7;

        then

         A7: (F . z) = x by TARSKI:def 1;

        z in ( dom F) by A5, FUNCT_1:def 7;

        then

         A8: z in (( dom (X --> x)) \/ ( dom (Y --> y)));

        assume

         A9: not z in X;

        (F . z) = ((Y --> y) . z) by A9, A8, FUNCT_4:def 1;

        hence contradiction by A3, A9, A6, A7, FUNCOP_1: 7;

      end;

      X c= (F " {x})

      proof

        let z be object such that

         A10: z in X;



         A11: z in ( dom F) by A1, A10, XBOOLE_0:def 3;

        z in ( dom (X --> x)) by A10;

        then

         A12: (F . z) = ((X --> x) . z) by FUNCT_4: 13;

        ((X --> x) . z) = x by A10, FUNCOP_1: 7;

        then (F . z) in {x} by A12, TARSKI:def 1;

        hence thesis by A11, FUNCT_1:def 7;

      end;

      then X = (F " {x}) by A4;

      hence thesis by Def1;

    end;

    theorem :: CARD_FIN:18



     Th17: x <> y & X misses Y implies ((X --> x) +* (Y --> y)) in ( Choose ((X \/ Y),( card X),x,y))

    proof

      assume that

       A1: x <> y and

       A2: X misses Y;

      ( dom (X --> x)) = X & ( dom (Y --> y)) = Y;

      then ((X --> x) +* (Y --> y)) = ((Y --> y) +* (X --> x)) by A2, FUNCT_4: 35;

      hence thesis by A1, Th16;

    end;

    definition

      let F,Ch be Function, y be object;

      :: CARD_FIN:def2

      func Intersection (F,Ch,y) -> Subset of ( union ( rng F)) means

      : Def2: z in it iff z in ( union ( rng F)) & for x st x in ( dom Ch) & (Ch . x) = y holds z in (F . x);

      existence

      proof

        defpred P[ object] means for x st x in ( dom Ch) & (Ch . x) = y holds $1 in (F . x);

        consider I be set such that

         A1: for z be object holds z in I iff z in ( union ( rng F)) & P[z] from XBOOLE_0:sch 1;

        I c= ( union ( rng F)) by A1;

        then

        reconsider I as Subset of ( union ( rng F));

        take I;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let I1,I2 be Subset of ( union ( rng F)) such that

         A2: z in I1 iff z in ( union ( rng F)) & for x st x in ( dom Ch) & (Ch . x) = y holds z in (F . x) and

         A3: z in I2 iff z in ( union ( rng F)) & for x st x in ( dom Ch) & (Ch . x) = y holds z in (F . x);

        for z be object holds z in I1 iff z in I2

        proof

          let z be object;

          z in I1 iff z in ( union ( rng F)) & for x st x in ( dom Ch) & (Ch . x) = y holds z in (F . x) by A2;

          hence thesis by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    reserve F,Ch for Function;

    theorem :: CARD_FIN:19



     Th18: for F, Ch st (( dom F) /\ (Ch " {x})) is non empty holds y in ( Intersection (F,Ch,x)) iff for z st z in ( dom Ch) & (Ch . z) = x holds y in (F . z)

    proof

      let F, Ch such that

       A1: (( dom F) /\ (Ch " {x})) is non empty;

      thus y in ( Intersection (F,Ch,x)) implies for z st z in ( dom Ch) & (Ch . z) = x holds y in (F . z) by Def2;

      thus (for z st z in ( dom Ch) & (Ch . z) = x holds y in (F . z)) implies y in ( Intersection (F,Ch,x))

      proof

        consider z be object such that

         A2: z in (( dom F) /\ (Ch " {x})) by A1;



         A3: z in (Ch " {x}) by A2, XBOOLE_0:def 4;

        then (Ch . z) in {x} by FUNCT_1:def 7;

        then

         A4: (Ch . z) = x by TARSKI:def 1;

        z in ( dom F) by A2, XBOOLE_0:def 4;

        then

         A5: (F . z) in ( rng F) by FUNCT_1:def 3;

        assume

         A6: for z st z in ( dom Ch) & (Ch . z) = x holds y in (F . z);

        z in ( dom Ch) by A3, FUNCT_1:def 7;

        then y in (F . z) by A6, A4;

        then y in ( union ( rng F)) by A5, TARSKI:def 4;

        hence thesis by A6, Def2;

      end;

    end;

    theorem :: CARD_FIN:20



     Th19: ( Intersection (F,Ch,y)) is non empty implies (Ch " {y}) c= ( dom F)

    proof

      assume ( Intersection (F,Ch,y)) is non empty;

      then

      consider z be object such that

       A1: z in ( Intersection (F,Ch,y));

      assume not (Ch " {y}) c= ( dom F);

      then

      consider x be object such that

       A2: x in (Ch " {y}) and

       A3: not x in ( dom F);

      (Ch . x) in {y} by A2, FUNCT_1:def 7;

      then

       A4: (Ch . x) = y by TARSKI:def 1;

      x in ( dom Ch) by A2, FUNCT_1:def 7;

      then z in (F . x) by A1, A4, Def2;

      hence thesis by A3, FUNCT_1:def 2;

    end;

    theorem :: CARD_FIN:21

    ( Intersection (F,Ch,y)) is non empty implies for x1, x2 st x1 in (Ch " {y}) & x2 in (Ch " {y}) holds (F . x1) meets (F . x2)

    proof

      assume ( Intersection (F,Ch,y)) is non empty;

      then

      consider z be object such that

       A1: z in ( Intersection (F,Ch,y));

      let x1, x2 such that

       A2: x1 in (Ch " {y}) and

       A3: x2 in (Ch " {y});

      (Ch . x2) in {y} by A3, FUNCT_1:def 7;

      then

       A4: (Ch . x2) = y by TARSKI:def 1;

      (Ch . x1) in {y} by A2, FUNCT_1:def 7;

      then

       A5: (Ch . x1) = y by TARSKI:def 1;

      x2 in ( dom Ch) by A3, FUNCT_1:def 7;

      then

       A6: z in (F . x2) by A1, A4, Def2;

      x1 in ( dom Ch) by A2, FUNCT_1:def 7;

      then z in (F . x1) by A1, A5, Def2;

      hence thesis by A6, XBOOLE_0: 3;

    end;

    theorem :: CARD_FIN:22



     Th21: z in ( Intersection (F,Ch,y)) & y in ( rng Ch) implies ex x st x in ( dom Ch) & (Ch . x) = y & z in (F . x)

    proof

      assume that

       A1: z in ( Intersection (F,Ch,y)) and

       A2: y in ( rng Ch);

      (Ch " {y}) <> {} by A2, FUNCT_1: 72;

      then

      consider x be object such that

       A3: x in (Ch " {y}) by XBOOLE_0:def 1;

      (Ch . x) in {y} by A3, FUNCT_1:def 7;

      then

       A4: (Ch . x) = y by TARSKI:def 1;



       A5: x in ( dom Ch) by A3, FUNCT_1:def 7;

      x in ( dom Ch) by A3, FUNCT_1:def 7;

      then z in (F . x) by A1, A4, Def2;

      hence thesis by A4, A5;

    end;

    theorem :: CARD_FIN:23

    F is empty or ( union ( rng F)) is empty implies ( Intersection (F,Ch,y)) = ( union ( rng F)) by RELAT_1: 38, ZFMISC_1: 2;

    theorem :: CARD_FIN:24



     Th23: for y be object holds (F | (Ch " {y})) = ((Ch " {y}) --> ( union ( rng F))) implies ( Intersection (F,Ch,y)) = ( union ( rng F))

    proof

      let y be object;

      set ChF = ((Ch " {y}) --> ( union ( rng F)));

      assume

       A1: (F | (Ch " {y})) = ChF;

      ( union ( rng F)) c= ( Intersection (F,Ch,y))

      proof

        let z be object such that

         A2: z in ( union ( rng F));

        now

          let x such that

           A3: x in ( dom Ch) and

           A4: (Ch . x) = y;

          (Ch . x) in {y} by A4, TARSKI:def 1;

          then

           A5: x in (Ch " {y}) by A3, FUNCT_1:def 7;

          then ( dom ChF) = (Ch " {y}) & (ChF . x) = ( union ( rng F)) by FUNCOP_1: 7;

          hence z in (F . x) by A1, A2, A5, FUNCT_1: 47;

        end;

        hence thesis by A2, Def2;

      end;

      hence thesis;

    end;

    theorem :: CARD_FIN:25

    ( union ( rng F)) is non empty & ( Intersection (F,Ch,y)) = ( union ( rng F)) implies (F | (Ch " {y})) = ((Ch " {y}) --> ( union ( rng F)))

    proof

      set ChF = ((Ch " {y}) --> ( union ( rng F)));

      assume that

       A1: ( union ( rng F)) is non empty and

       A2: ( Intersection (F,Ch,y)) = ( union ( rng F));



       A3: (( dom F) /\ (Ch " {y})) = ( dom (F | (Ch " {y}))) by RELAT_1: 61;

      (( dom F) /\ (Ch " {y})) = (Ch " {y}) by A1, A2, Th19, XBOOLE_1: 28;

      then

       A4: ( dom (F | (Ch " {y}))) = ( dom ChF) by A3;

      assume (F | (Ch " {y})) <> ChF;

      then

      consider x be object such that

       A5: x in ( dom (F | (Ch " {y}))) and

       A6: ((F | (Ch " {y})) . x) <> (ChF . x) by A4;

      x in (( dom F) /\ (Ch " {y})) by A5, RELAT_1: 61;

      then

       A7: x in ( dom F) by XBOOLE_0:def 4;

      x in (( dom F) /\ (Ch " {y})) by A5, RELAT_1: 61;

      then

       A8: x in (Ch " {y}) by XBOOLE_0:def 4;

      then

       A9: (ChF . x) = ( union ( rng F)) by FUNCOP_1: 7;

      (Ch . x) in {y} by A8, FUNCT_1:def 7;

      then

       A10: (Ch . x) = y by TARSKI:def 1;

      (F . x) = ((F | (Ch " {y})) . x) by A5, FUNCT_1: 47;

      then ((F | (Ch " {y})) . x) in ( rng F) by A7, FUNCT_1:def 3;

      then ((F | (Ch " {y})) . x) c= (ChF . x) by A9, ZFMISC_1: 74;

      then not ( union ( rng F)) c= ((F | (Ch " {y})) . x) by A6, A9;

      then

      consider z be object such that

       A11: z in ( union ( rng F)) and

       A12: not z in ((F | (Ch " {y})) . x);

      x in ( dom Ch) by A8, FUNCT_1:def 7;

      then z in (F . x) by A2, A11, A10, Def2;

      hence thesis by A5, A12, FUNCT_1: 47;

    end;

    theorem :: CARD_FIN:26



     Th25: for y be object holds ( Intersection (F, {} ,y)) = ( union ( rng F))

    proof

      let y be object;

      (F | ( {} " {y}) qua set) = (( {} " {y}) --> ( union ( rng F)));

      hence thesis by Th23;

    end;

    theorem :: CARD_FIN:27



     Th26: for y be object holds ( Intersection (F,Ch,y)) c= ( Intersection (F,(Ch | X9),y))

    proof

      let y be object;

      let z be object such that

       A1: z in ( Intersection (F,Ch,y));

      now

        let x such that

         A2: x in ( dom (Ch | X9)) and

         A3: ((Ch | X9) . x) = y;

        x in (( dom Ch) /\ X9) by A2, RELAT_1: 61;

        then

         A4: x in ( dom Ch) by XBOOLE_0:def 4;

        (Ch . x) = y by A2, A3, FUNCT_1: 47;

        hence z in (F . x) by A1, A4, Def2;

      end;

      hence thesis by A1, Def2;

    end;

    theorem :: CARD_FIN:28



     Th27: (Ch " {y}) = ((Ch | X9) " {y}) implies ( Intersection (F,Ch,y)) = ( Intersection (F,(Ch | X9),y))

    proof

      assume

       A1: (Ch " {y}) = ((Ch | X9) " {y});



       A2: ( Intersection (F,(Ch | X9),y)) c= ( Intersection (F,Ch,y))

      proof

        let z be object such that

         A3: z in ( Intersection (F,(Ch | X9),y));

        now

          let x such that

           A4: x in ( dom Ch) and

           A5: (Ch . x) = y;

          (Ch . x) in {y} by A5, TARSKI:def 1;

          then

           A6: x in ((Ch | X9) " {y}) by A1, A4, FUNCT_1:def 7;

          then ((Ch | X9) . x) in {y} by FUNCT_1:def 7;

          then

           A7: ((Ch | X9) . x) = y by TARSKI:def 1;

          x in ( dom (Ch | X9)) by A6, FUNCT_1:def 7;

          hence z in (F . x) by A3, A7, Def2;

        end;

        hence thesis by A3, Def2;

      end;

      ( Intersection (F,Ch,y)) c= ( Intersection (F,(Ch | X9),y)) by Th26;

      hence thesis by A2;

    end;

    theorem :: CARD_FIN:29



     Th28: ( Intersection ((F | X9),Ch,y)) c= ( Intersection (F,Ch,y))

    proof

      let z be object such that

       A1: z in ( Intersection ((F | X9),Ch,y));

       A2:

      now



         A3: (Ch " {y}) c= ( dom (F | X9)) by A1, Th19;

        let x such that

         A4: x in ( dom Ch) and

         A5: (Ch . x) = y;

        (Ch . x) in {y} by A5, TARSKI:def 1;

        then

         A6: x in (Ch " {y}) by A4, FUNCT_1:def 7;

        z in ((F | X9) . x) by A1, A4, A5, Def2;

        hence z in (F . x) by A6, A3, FUNCT_1: 47;

      end;

      ( union ( rng (F | X9))) c= ( union ( rng F)) & z in ( union ( rng (F | X9))) by A1, RELAT_1: 70, ZFMISC_1: 77;

      hence thesis by A2, Def2;

    end;

    theorem :: CARD_FIN:30



     Th29: y in ( rng Ch) & (Ch " {y}) c= X9 implies ( Intersection ((F | X9),Ch,y)) = ( Intersection (F,Ch,y))

    proof

      assume that

       A1: y in ( rng Ch) and

       A2: (Ch " {y}) c= X9;



       A3: ( Intersection (F,Ch,y)) c= ( Intersection ((F | X9),Ch,y))

      proof

        let z be object such that

         A4: z in ( Intersection (F,Ch,y));

         A5:

        now

          let x such that

           A6: x in ( dom Ch) and

           A7: (Ch . x) = y;

          (Ch . x) in {y} by A7, TARSKI:def 1;

          then

           A8: x in (Ch " {y}) by A6, FUNCT_1:def 7;

          z in (F . x) by A4, A6, A7, Def2;

          then x in ( dom F) by FUNCT_1:def 2;

          then x in (( dom F) /\ X9) by A2, A8, XBOOLE_0:def 4;

          then

           A9: x in ( dom (F | X9)) by RELAT_1: 61;

          z in (F . x) by A4, A6, A7, Def2;

          hence z in ((F | X9) . x) by A9, FUNCT_1: 47;

        end;

        consider x such that

         A10: x in ( dom Ch) and

         A11: (Ch . x) = y and

         A12: z in (F . x) by A1, A4, Th21;

        (Ch . x) in {y} by A11, TARSKI:def 1;

        then

         A13: x in (Ch " {y}) by A10, FUNCT_1:def 7;

        x in ( dom F) by A12, FUNCT_1:def 2;

        then x in (( dom F) /\ X9) by A2, A13, XBOOLE_0:def 4;

        then x in ( dom (F | X9)) by RELAT_1: 61;

        then

         A14: ((F | X9) . x) in ( rng (F | X9)) by FUNCT_1:def 3;

        z in ((F | X9) . x) by A5, A10, A11;

        then z in ( union ( rng (F | X9))) by A14, TARSKI:def 4;

        hence thesis by A5, Def2;

      end;

      ( Intersection ((F | X9),Ch,y)) c= ( Intersection (F,Ch,y)) by Th28;

      hence thesis by A3;

    end;

    theorem :: CARD_FIN:31



     Th30: for x,y be object holds x in (Ch " {y}) implies ( Intersection (F,Ch,y)) c= (F . x)

    proof

      let x,y be object;

      assume

       A1: x in (Ch " {y});

      then

       A2: x in ( dom Ch) by FUNCT_1:def 7;

      (Ch . x) in {y} by A1, FUNCT_1:def 7;

      then

       A3: (Ch . x) = y by TARSKI:def 1;

      let z be object;

      assume z in ( Intersection (F,Ch,y));

      hence thesis by A2, A3, Def2;

    end;

    theorem :: CARD_FIN:32



     Th31: for x,y be object holds x in (Ch " {y}) implies (( Intersection (F,(Ch | (( dom Ch) \ {x})),y)) /\ (F . x)) = ( Intersection (F,Ch,y))

    proof

      let x,y be object;

      set d = (( dom Ch) \ {x});

      set Chd = (Ch | d);

      set I1 = ( Intersection (F,Ch,y));

      set I2 = ( Intersection (F,Chd,y));

      assume x in (Ch " {y});

      then

       A1: I1 c= (F . x) by Th30;



       A2: (I2 /\ (F . x)) c= I1

      proof

        let z be object such that

         A3: z in (I2 /\ (F . x));

        now

          let x1 such that

           A4: x1 in ( dom Ch) and

           A5: (Ch . x1) = y;

          per cases by A4, XBOOLE_0:def 5;

            suppose

             A6: x1 in d;



             A7: z in I2 by A3, XBOOLE_0:def 4;



             A8: (( dom Ch) /\ d) = ( dom Chd) & (( dom Ch) /\ d) = d by RELAT_1: 61, XBOOLE_1: 28;

            then (Chd . x1) = y by A5, A6, FUNCT_1: 47;

            hence z in (F . x1) by A6, A8, A7, Def2;

          end;

            suppose x1 in {x};

            then x1 = x by TARSKI:def 1;

            hence z in (F . x1) by A3, XBOOLE_0:def 4;

          end;

        end;

        hence thesis by A3, Def2;

      end;

      I1 c= I2 by Th26;

      then I1 c= (I2 /\ (F . x)) by A1, XBOOLE_1: 19;

      hence thesis by A2;

    end;

    theorem :: CARD_FIN:33



     Th32: for x1,x2 be object holds for Ch1,Ch2 be Function st (Ch1 " {x1}) = (Ch2 " {x2}) holds ( Intersection (F,Ch1,x1)) = ( Intersection (F,Ch2,x2))

    proof

      let x1,x2 be object;

      let Ch1,Ch2 be Function such that

       A1: (Ch1 " {x1}) = (Ch2 " {x2});

      thus ( Intersection (F,Ch1,x1)) c= ( Intersection (F,Ch2,x2))

      proof

        let z be object such that

         A2: z in ( Intersection (F,Ch1,x1));

        now

          let x such that

           A3: x in ( dom Ch2) and

           A4: (Ch2 . x) = x2;

          (Ch2 . x) in {x2} by A4, TARSKI:def 1;

          then

           A5: x in (Ch1 " {x1}) by A1, A3, FUNCT_1:def 7;

          then (Ch1 . x) in {x1} by FUNCT_1:def 7;

          then

           A6: (Ch1 . x) = x1 by TARSKI:def 1;

          x in ( dom Ch1) by A5, FUNCT_1:def 7;

          hence z in (F . x) by A2, A6, Def2;

        end;

        hence thesis by A2, Def2;

      end;

      thus ( Intersection (F,Ch2,x2)) c= ( Intersection (F,Ch1,x1))

      proof

        let z be object such that

         A7: z in ( Intersection (F,Ch2,x2));

        now

          let x such that

           A8: x in ( dom Ch1) and

           A9: (Ch1 . x) = x1;

          (Ch1 . x) in {x1} by A9, TARSKI:def 1;

          then

           A10: x in (Ch2 " {x2}) by A1, A8, FUNCT_1:def 7;

          then (Ch2 . x) in {x2} by FUNCT_1:def 7;

          then

           A11: (Ch2 . x) = x2 by TARSKI:def 1;

          x in ( dom Ch2) by A10, FUNCT_1:def 7;

          hence z in (F . x) by A7, A11, Def2;

        end;

        hence thesis by A7, Def2;

      end;

    end;

    theorem :: CARD_FIN:34



     Th33: for y be object holds (Ch " {y}) = {} implies ( Intersection (F,Ch,y)) = ( union ( rng F))

    proof

      let y be object;

      reconsider E = {} as set;



       A1: (Ch | E) = {} & ( Intersection (F, {} ,y)) = ( union ( rng F)) by Th25;

      assume (Ch " {y}) = {} ;

      then ((Ch | E) " {y}) = (Ch " {y});

      hence thesis by A1, Th32;

    end;

    theorem :: CARD_FIN:35



     Th34: for x,y be object holds {x} = (Ch " {y}) implies ( Intersection (F,Ch,y)) = (F . x)

    proof

      let x,y be object;



       A1: (( dom Ch) \ {x}) misses {x} by XBOOLE_1: 79;

      assume

       A2: {x} = (Ch " {y});

      then ((Ch | (( dom Ch) \ {x})) " {y}) = ((( dom Ch) \ {x}) /\ {x}) by FUNCT_1: 70;

      then ((Ch | (( dom Ch) \ {x})) " {y}) = {} by A1;

      then

       A3: ( Intersection (F,(Ch | (( dom Ch) \ {x})),y)) = ( union ( rng F)) by Th33;

      x in (Ch " {y}) by A2, TARSKI:def 1;

      then

       A4: (( union ( rng F)) /\ (F . x)) = ( Intersection (F,Ch,y)) by A3, Th31;

      per cases ;

        suppose x in ( dom F);

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

        hence thesis by A4, XBOOLE_1: 28, ZFMISC_1: 74;

      end;

        suppose not x in ( dom F);

        then (F . x) = {} by FUNCT_1:def 2;

        hence thesis by A4;

      end;

    end;

    theorem :: CARD_FIN:36



     Th35: {x1, x2} = (Ch " {y}) implies ( Intersection (F,Ch,y)) = ((F . x1) /\ (F . x2))

    proof

      assume

       A1: {x1, x2} = (Ch " {y});

      per cases ;

        suppose

         A2: x1 = x2;

        then (Ch " {y}) = {x1} by A1, ENUMSET1: 29;

        hence thesis by A2, Th34;

      end;

        suppose

         A3: x1 <> x2;

        ((Ch " {y}) /\ (( dom Ch) \ {x1})) = (((Ch " {y}) /\ ( dom Ch)) \ {x1}) & ((Ch " {y}) /\ ( dom Ch)) = {x1, x2} by A1, RELAT_1: 132, XBOOLE_1: 28, XBOOLE_1: 49;

        then ((Ch " {y}) /\ (( dom Ch) \ {x1})) = {x2} by A3, ZFMISC_1: 17;

        then

         A4: ((Ch | (( dom Ch) \ {x1})) " {y}) = {x2} by FUNCT_1: 70;

        x1 in (Ch " {y}) by A1, TARSKI:def 2;

        then (( Intersection (F,(Ch | (( dom Ch) \ {x1})),y)) /\ (F . x1)) = ( Intersection (F,Ch,y)) by Th31;

        hence thesis by A4, Th34;

      end;

    end;

    theorem :: CARD_FIN:37

    for F st F is non empty holds y in ( Intersection (F,(( dom F) --> x),x)) iff for z st z in ( dom F) holds y in (F . z)

    proof

      let F such that

       A1: F is non empty;

      set Ch = (( dom F) --> x);

      thus y in ( Intersection (F,Ch,x)) implies for z st z in ( dom F) holds y in (F . z)

      proof

        assume

         A2: y in ( Intersection (F,Ch,x));

        let z;

        assume z in ( dom F);

        then z in ( dom Ch) & (Ch . z) = x by FUNCOP_1: 7;

        hence thesis by A2, Def2;

      end;

      (Ch " {x}) = ( dom F) by FUNCOP_1: 15;

      then

       A3: (( dom F) /\ (Ch " {x})) = ( dom F);

      assume for z st z in ( dom F) holds y in (F . z);

      then for z st z in ( dom Ch) & (Ch . z) = x holds y in (F . z);

      hence thesis by A1, A3, Th18;

    end;

    registration

      let F be finite-yielding Function, X be set;

      cluster (F | X) -> finite-yielding;

      coherence

      proof

        let x be object;

        assume x in ( dom (F | X));

        then ((F | X) . x) = (F . x) by FUNCT_1: 47;

        hence thesis;

      end;

    end

    registration

      let F be finite-yielding Function, G be Function;

      cluster (F * G) -> finite-yielding;

      coherence

      proof

        let x be object;

        assume x in ( dom (F * G));

        then ((F * G) . x) = (F . (G . x)) by FUNCT_1: 12;

        hence thesis;

      end;

      cluster ( Intersect (F,G)) -> finite-yielding;

      coherence

      proof

        let x be object;

        assume x in ( dom ( Intersect (F,G)));

        then x in (( dom F) /\ ( dom G)) by YELLOW20:def 2;

        then (( Intersect (F,G)) . x) = ((F . x) /\ (G . x)) by YELLOW20:def 2;

        hence thesis;

      end;

    end

    reserve Fy for finite-yielding Function;

    theorem :: CARD_FIN:38

    y in ( rng Ch) implies ( Intersection (Fy,Ch,y)) is finite

    proof

      assume y in ( rng Ch);

      then

      consider x be object such that

       A1: x in ( dom Ch) and

       A2: (Ch . x) = y by FUNCT_1:def 3;

      (Ch . x) in {y} by A2, TARSKI:def 1;

      then x in (Ch " {y}) by A1, FUNCT_1:def 7;

      then ( Intersection (Fy,Ch,y)) c= (Fy . x) by Th30;

      hence thesis;

    end;

    theorem :: CARD_FIN:39



     Th38: ( dom Fy) is finite implies ( union ( rng Fy)) is finite

    proof

      assume ( dom Fy) is finite;

      then ( rng Fy) is finite by FINSET_1: 8;

      hence thesis;

    end;

    theorem :: CARD_FIN:40

    x in ( Choose (n,k,1, 0 )) iff ex F be XFinSequence of NAT st F = x & ( dom F) = n & ( rng F) c= { 0 , 1} & ( Sum F) = k

    proof

      thus x in ( Choose (n,k,1, 0 )) implies ex F be XFinSequence of NAT st F = x & ( dom F) = n & ( rng F) c= { 0 , 1} & ( Sum F) = k

      proof

        assume x in ( Choose (n,k,1, 0 ));

        then

        consider F be Function of n, { 0 , 1} such that

         A1: x = F & ( card (F " {1})) = k by Def1;



         A2: ( rng F) c= { 0 , 1};

        ( dom F) = n by FUNCT_2:def 1;

        then

        reconsider F as XFinSequence by AFINSQ_1: 5;

        ( rng F) is Subset of NAT by A2, XBOOLE_1: 1;

        then

        reconsider F as XFinSequence of NAT by RELAT_1:def 19;

        take F;

        ( Sum F) = (1 * ( card (F " {1}))) by A2, AFINSQ_2: 68;

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

      end;

      given F be XFinSequence of NAT such that

       A3: F = x and

       A4: ( dom F) = n & ( rng F) c= { 0 , 1} & ( Sum F) = k;

      (1 * ( card (F " {1}))) = k & F is Function of n, { 0 , 1} by A4, AFINSQ_2: 68, FUNCT_2: 2;

      hence thesis by A3, Def1;

    end;



     Lm2: ex P be Function of ( card X), X st P is one-to-one

    proof

      (( card X),X) are_equipotent by CARD_1:def 2;

      then

      consider P be Function such that

       A1: P is one-to-one and

       A2: ( dom P) = ( card X) & ( rng P) = X by WELLORD2:def 4;

      P is Function of ( card X), X by A2, FUNCT_2: 1;

      hence thesis by A1;

    end;

    definition

      ::$Canceled

      let k;

      let F be finite-yielding Function;

      assume

       A1: ( dom F) is finite;

      :: CARD_FIN:def4

      func Card_Intersection (F,k) -> Element of NAT means

      : Def3: for x,y be object, X be finite set, P be Function of ( card ( Choose (X,k,x,y))), ( Choose (X,k,x,y)) st ( dom F) = X & P is one-to-one & x <> y holds ex XFS be XFinSequence of NAT st ( dom XFS) = ( dom P) & (for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (F,f,x)))) & it = ( Sum XFS);

      existence

      proof

        reconsider D = ( dom F) as finite set by A1;

        set Ch1 = ( Choose (D,k, 0 ,1));

        (( card Ch1),Ch1) are_equipotent by CARD_1:def 2;

        then

        consider P1 be Function such that

         A2: P1 is one-to-one and

         A3: ( dom P1) = ( card Ch1) and

         A4: ( rng P1) = Ch1 by WELLORD2:def 4;

        reconsider P1 as Function of ( card Ch1), Ch1 by A3, A4, FUNCT_2: 1;

        defpred xfs1[ object, object] means for f st f = (P1 . $1) holds $2 = ( card ( Intersection (F,f, 0 )));



         A5: for x be object st x in ( card Ch1) holds ex y be object st y in NAT & xfs1[x, y]

        proof

          let x be object;

          assume x in ( card Ch1);

          then x in ( dom P1) by CARD_1: 27, FUNCT_2:def 1;

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

          then

          consider f be Function of D, { 0 , 1} such that

           A6: f = (P1 . x) and ( card (f " { 0 })) = k by Def1;

          ( union ( rng F)) is finite by A1, Th38;

          then

          reconsider I = ( Intersection (F,f, 0 )) as finite set;

          take ( card I);

          thus thesis by A6;

        end;

        consider XFS1 be Function of ( card Ch1), NAT such that

         A7: for x be object st x in ( card Ch1) holds xfs1[x, (XFS1 . x)] from FUNCT_2:sch 1( A5);



         A8: ( dom XFS1) = ( card Ch1) by FUNCT_2:def 1;

        then

        reconsider XFS1 as XFinSequence by AFINSQ_1: 5;

        reconsider XFS1 as XFinSequence of NAT ;

        reconsider S = ( Sum XFS1) as Element of NAT by ORDINAL1:def 12;

        take S;

        let x,y be object, X be finite set, P be Function of ( card ( Choose (X,k,x,y))), ( Choose (X,k,x,y)) such that

         A9: ( dom F) = X and

         A10: P is one-to-one and

         A11: x <> y;

        defpred perm[ object, object] means for f1 be Function of D, { 0 , 1}, f be Function of X, {x, y} st f1 = (P1 . $1) & f = (P . $2) holds (f1 " { 0 }) = (f " {x}) & for z st z in X holds ((f1 . z) = 0 iff (f . z) = x) & ((f1 . z) = 1 iff (f . z) = y);

        set Ch = ( Choose (X,k,x,y));



         A12: for x1 be object st x1 in ( card Ch1) holds ex x2 be object st x2 in ( card Ch1) & perm[x1, x2]

        proof

          ( card ( card ( Choose (X,k,x,y)))) = ( card ( Choose (X,k,x,y)));

          then P is onto by A10, FINSEQ_4: 63;

          then

           A13: ( rng P) = Ch by FUNCT_2:def 3;

          let x1 be object;

          assume x1 in ( card Ch1);

          then (P1 . x1) in ( rng P1) by A3, FUNCT_1:def 3;

          then

          consider f1 be Function of D, { 0 , 1} such that

           A14: f1 = (P1 . x1) and

           A15: ( card (f1 " { 0 })) = k by Def1;

          defpred pf[ object, object] means ((f1 . $1) = 0 iff $2 = x) & ((f1 . $1) = 1 iff $2 = y);



           A16: for d be object st d in X holds ex fd be object st fd in {x, y} & pf[d, fd]

          proof

            let d be object;

            assume d in X;

            then d in ( dom f1) by A9, FUNCT_2:def 1;

            then (f1 . d) in ( rng f1) by FUNCT_1:def 3;

            then

             A17: (f1 . d) = 0 or (f1 . d) = 1 by TARSKI:def 2;

            x in {x, y} & y in {x, y} by TARSKI:def 2;

            hence thesis by A11, A17;

          end;

          consider f be Function of X, {x, y} such that

           A18: for d be object st d in X holds pf[d, (f . d)] from FUNCT_2:sch 1( A16);



           A19: ( dom f1) = D by FUNCT_2:def 1;



           A20: (f1 " { 0 }) c= (f " {x})

          proof

            let z be object;

            assume

             A21: z in (f1 " { 0 });

            then (f1 . z) in { 0 } by FUNCT_1:def 7;

            then

             A22: (f1 . z) = 0 by TARSKI:def 1;



             A23: ( dom f1) = ( dom f) by A9, A19, FUNCT_2:def 1;

            then z in ( dom f) by A19, A21;

            then (f . z) = x by A18, A22;

            then (f . z) in {x} by TARSKI:def 1;

            hence thesis by A19, A21, A23, FUNCT_1:def 7;

          end;



           A24: (f " {x}) c= (f1 " { 0 })

          proof

            let z be object;

            assume

             A25: z in (f " {x});

            then (f . z) in {x} by FUNCT_1:def 7;

            then (f . z) = x by TARSKI:def 1;

            then (f1 . z) = 0 by A18, A25;

            then (f1 . z) in { 0 } by TARSKI:def 1;

            hence thesis by A9, A19, A25, FUNCT_1:def 7;

          end;

          then (f " {x}) = (f1 " { 0 }) by A20;

          then f in Ch by A15, Def1;

          then

          consider x2 be object such that

           A26: x2 in ( dom P) and

           A27: (P . x2) = f by A13, FUNCT_1:def 3;

          reconsider x2 as set by TARSKI: 1;

          take x2;

          ( card Ch) = (( card X) choose k) & ( card Ch1) = (( card D) choose k) by A11, Th15;

          hence x2 in ( card Ch1) by A9, A26;

          let f19 be Function of D, { 0 , 1}, f9 be Function of X, {x, y} such that

           A28: f19 = (P1 . x1) & f9 = (P . x2);

          thus (f9 " {x}) = (f19 " { 0 }) by A14, A24, A20, A27, A28;

          let z;

          assume z in X;

          hence thesis by A14, A18, A27, A28;

        end;

        consider Perm be Function of ( card Ch1), ( card Ch1) such that

         A29: for x1 be object st x1 in ( card Ch1) holds perm[x1, (Perm . x1)] from FUNCT_2:sch 1( A12);

        now



           A30: Ch = {} implies ( card Ch) = {} ;

          let z1,z2 be object such that

           A31: z1 in ( dom Perm) and

           A32: z2 in ( dom Perm) and

           A33: (Perm . z1) = (Perm . z2);



           A34: ( card X) = ( card D) by A9;

          ( card Ch) = (( card X) choose k) & ( card Ch1) = (( card D) choose k) by A11, Th15;

          then ( card Ch1) = ( card Ch) by A34;

          then (Perm . z1) in ( card Ch) by A31, FUNCT_2: 5;

          then (Perm . z1) in ( dom P) by A30, FUNCT_2:def 1;

          then (P . (Perm . z1)) in ( rng P) by FUNCT_1:def 3;

          then

          consider PPermz1 be Function of X, {x, y} such that

           A35: PPermz1 = (P . (Perm . z1)) and ( card (PPermz1 " {x})) = k by Def1;

          (P1 . z2) in ( rng P1) by A3, A32, FUNCT_1:def 3;

          then

          consider P1z2 be Function of D, { 0 , 1} such that

           A36: (P1 . z2) = P1z2 and ( card (P1z2 " { 0 })) = k by Def1;

          (P1 . z1) in ( rng P1) by A3, A31, FUNCT_1:def 3;

          then

          consider P1z1 be Function of D, { 0 , 1} such that

           A37: (P1 . z1) = P1z1 and ( card (P1z1 " { 0 })) = k by Def1;



           A38: for z be object st z in ( dom P1z1) holds (P1z1 . z) = (P1z2 . z)

          proof

            let z be object such that

             A39: z in ( dom P1z1);



             A40: (P1z1 . z) in ( rng P1z1) by A39, FUNCT_1:def 3;

            per cases by A40, TARSKI:def 2;

              suppose

               A41: (P1z1 . z) = 0 ;

              then (PPermz1 . z) = x by A9, A29, A31, A37, A35, A39;

              hence thesis by A9, A29, A32, A33, A36, A35, A39, A41;

            end;

              suppose

               A42: (P1z1 . z) = 1;

              then (PPermz1 . z) = y by A9, A29, A31, A37, A35, A39;

              hence thesis by A9, A29, A32, A33, A36, A35, A39, A42;

            end;

          end;

          ( dom P1z1) = D & ( dom P1z2) = D by FUNCT_2:def 1;

          then P1z1 = P1z2 by A38;

          hence z1 = z2 by A2, A3, A31, A32, A37, A36;

        end;

        then

         A43: Perm is one-to-one;

        ( card ( card Ch1)) = ( card ( card Ch1));

        then

         A44: Perm is one-to-one onto by A43, FINSEQ_4: 63;

        defpred xfs[ object, object] means for f st f = (P . $1) holds $2 = ( card ( Intersection (F,f,x)));



         A45: for x1 be object st x1 in ( card Ch) holds ex x2 be object st x2 in NAT & xfs[x1, x2]

        proof

          let x1 be object;

          assume x1 in ( card Ch);

          then x1 in ( dom P) by CARD_1: 27, FUNCT_2:def 1;

          then (P . x1) in ( rng P) by FUNCT_1:def 3;

          then

          consider f be Function of X, {x, y} such that

           A46: f = (P . x1) and ( card (f " {x})) = k by Def1;

          ( union ( rng F)) is finite by A1, Th38;

          then

          reconsider I = ( Intersection (F,f,x)) as finite set;

          take ( card I);

          thus thesis by A46;

        end;

        consider XFS be Function of ( card Ch), NAT such that

         A47: for x1 be object st x1 in ( card Ch) holds xfs[x1, (XFS . x1)] from FUNCT_2:sch 1( A45);



         A48: ( dom XFS) = ( card Ch) by FUNCT_2:def 1;

        then

        reconsider XFS as XFinSequence by AFINSQ_1: 5;

        reconsider XFS as XFinSequence of NAT ;

        take XFS;

        Ch = {} implies ( card Ch) = {} ;

        then ( dom P) = ( card Ch) by FUNCT_2:def 1;

        hence

         A49: ( dom XFS) = ( dom P) by FUNCT_2:def 1;

        hence for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (F,f,x))) by A47;



         A50: ( card Ch1) = (( card D) choose k) by Th15;



         A51: ( card Ch) = (( card X) choose k) by A11, Th15;

        then ( card Ch1) = ( dom XFS) by A9, A50, FUNCT_2:def 1;

        then

        reconsider Perm as Permutation of ( dom XFS) by A44;



         A52: ( dom XFS) = ( dom XFS1) by A9, A48, A50, A51, FUNCT_2:def 1;



         A53: for z be object st z in ( dom XFS1) holds (XFS1 . z) = ((XFS * Perm) . z)

        proof

          let z be object such that

           A54: z in ( dom XFS1);



           A55: z in ( dom Perm) by A8, A54, FUNCT_2: 52;



           A56: (Perm . z) in ( dom XFS) by A52, A54, FUNCT_2: 5;

          then (P . (Perm . z)) in ( rng P) by A49, FUNCT_1:def 3;

          then

          consider p be Function of X, {x, y} such that

           A57: p = (P . (Perm . z)) and ( card (p " {x})) = k by Def1;



           A58: (XFS . (Perm . z)) = ( card ( Intersection (F,p,x))) by A47, A48, A57, A56;

          (P1 . z) in ( rng P1) by A3, A8, A54, FUNCT_1:def 3;

          then

          consider p1 be Function of D, { 0 , 1} such that

           A59: p1 = (P1 . z) and ( card (p1 " { 0 })) = k by Def1;

          (p1 " { 0 }) = (p " {x}) by A8, A29, A54, A57, A59;

          then

           A60: ( Intersection (F,p1, 0 )) = ( Intersection (F,p,x)) by Th32;

          (XFS1 . z) = ( card ( Intersection (F,p1, 0 ))) by A7, A8, A54, A59;

          hence thesis by A60, A58, A55, FUNCT_1: 13;

        end;

        ( rng Perm) c= ( dom XFS) & ( dom Perm) = ( dom XFS) by FUNCT_2: 52;

        then ( dom XFS1) = ( dom (XFS * Perm)) by A52, RELAT_1: 27;

        then XFS1 = (XFS * Perm) by A53;

        then

         A61: ( addnat "**" XFS) = ( addnat "**" XFS1) by AFINSQ_2: 45;

        ( addnat "**" XFS1) = ( Sum XFS1) by AFINSQ_2: 51;

        hence thesis by A61, AFINSQ_2: 51;

      end;

      uniqueness

      proof

        reconsider D = ( dom F) as finite set by A1;

        let n1,n2 be Element of NAT such that

         A62: for x,y be object, X be finite set, P be Function of ( card ( Choose (X,k,x,y))), ( Choose (X,k,x,y)) st ( dom F) = X & P is one-to-one & x <> y holds ex XFS be XFinSequence of NAT st ( dom XFS) = ( dom P) & (for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (F,f,x)))) & n1 = ( Sum XFS) and

         A63: for x,y be object, X be finite set, P be Function of ( card ( Choose (X,k,x,y))), ( Choose (X,k,x,y)) st ( dom F) = X & P is one-to-one & x <> y holds ex XFS be XFinSequence of NAT st ( dom XFS) = ( dom P) & (for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (F,f,x)))) & n2 = ( Sum XFS);

        set Ch1 = ( Choose (D,k, 0 ,1));

        (( card Ch1),Ch1) are_equipotent by CARD_1:def 2;

        then

        consider P be Function such that

         A64: P is one-to-one and

         A65: ( dom P) = ( card Ch1) & ( rng P) = Ch1 by WELLORD2:def 4;

        reconsider P as Function of ( card Ch1), Ch1 by A65, FUNCT_2: 1;

        consider XFS1 be XFinSequence of NAT such that

         A66: ( dom XFS1) = ( dom P) and

         A67: for z, f st z in ( dom XFS1) & f = (P . z) holds (XFS1 . z) = ( card ( Intersection (F,f, 0 ))) and

         A68: n1 = ( Sum XFS1) by A62, A64;

        consider XFS2 be XFinSequence of NAT such that

         A69: ( dom XFS2) = ( dom P) and

         A70: for z, f st z in ( dom XFS2) & f = (P . z) holds (XFS2 . z) = ( card ( Intersection (F,f, 0 ))) and

         A71: n2 = ( Sum XFS2) by A63, A64;

        now

          let z be object such that

           A72: z in ( dom XFS1);

          (P . z) in ( rng P) by A66, A72, FUNCT_1:def 3;

          then

          consider Pz be Function of D, { 0 , 1} such that

           A73: Pz = (P . z) and ( card (Pz " { 0 })) = k by Def1;

          (XFS2 . z) = ( card ( Intersection (F,Pz, 0 ))) by A66, A69, A70, A72, A73;

          hence (XFS2 . z) = (XFS1 . z) by A67, A72, A73;

        end;

        hence thesis by A66, A68, A69, A71, FUNCT_1: 2;

      end;

    end

    theorem :: CARD_FIN:41

    for x,y be set, X be finite set, P be Function of ( card ( Choose (X,k,x,y))), ( Choose (X,k,x,y)) st ( dom Fy) = X & P is one-to-one & x <> y holds for XFS be XFinSequence of NAT st ( dom XFS) = ( dom P) & (for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (Fy,f,x)))) holds ( Card_Intersection (Fy,k)) = ( Sum XFS)

    proof

      let x,y be set, X be finite set, P be Function of ( card ( Choose (X,k,x,y))), ( Choose (X,k,x,y));

      assume ( dom Fy) = X & P is one-to-one & x <> y;

      then

      consider XFS be XFinSequence of NAT such that

       A1: ( dom XFS) = ( dom P) and

       A2: for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (Fy,f,x))) and

       A3: ( Card_Intersection (Fy,k)) = ( Sum XFS) by Def3;

      let XFS1 be XFinSequence of NAT such that

       A4: ( dom XFS1) = ( dom P) and

       A5: for z, f st z in ( dom XFS1) & f = (P . z) holds (XFS1 . z) = ( card ( Intersection (Fy,f,x)));

      now

        let z be object such that

         A6: z in ( dom XFS);

        (P . z) in ( rng P) by A1, A6, FUNCT_1:def 3;

        then

        consider Pz be Function of X, {x, y} such that

         A7: Pz = (P . z) and ( card (Pz " {x})) = k by Def1;

        (XFS1 . z) = ( card ( Intersection (Fy,Pz,x))) by A4, A5, A1, A6, A7;

        hence (XFS1 . z) = (XFS . z) by A2, A6, A7;

      end;

      hence thesis by A4, A1, A3, FUNCT_1: 2;

    end;

    theorem :: CARD_FIN:42

    ( dom Fy) is finite & k = 0 implies ( Card_Intersection (Fy,k)) = ( card ( union ( rng Fy)))

    proof

      assume that

       A1: ( dom Fy) is finite and

       A2: k = 0 ;

      reconsider X = ( dom Fy) as finite set by A1;

      set Ch = ( Choose (X,k, 0 ,1));

      consider P be Function of ( card Ch), Ch such that

       A3: P is one-to-one by Lm2;



       A4: ( card Ch) = 1 by A2, Th10;

      then

       A5: ( dom P) = 1 by CARD_1: 27, FUNCT_2:def 1;

      consider XFS be XFinSequence of NAT such that

       A6: ( dom XFS) = ( dom P) and

       A7: for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (Fy,f, 0 ))) and

       A8: ( Card_Intersection (Fy,k)) = ( Sum XFS) by A3, Def3;

      ( len XFS) = 1 by A6, A4, CARD_1: 27, FUNCT_2:def 1;

      then XFS = <%(XFS . 0 )%> by AFINSQ_1: 34;

      then

       A9: ( addnat "**" XFS) = (XFS . 0 ) by AFINSQ_2: 37;



       A10: 0 in 1 by CARD_1: 49, TARSKI:def 1;

      then (P . 0 ) in ( rng P) by A5, FUNCT_1:def 3;

      then

      consider P0 be Function of X, { 0 , 1} such that

       A11: P0 = (P . 0 ) and

       A12: ( card (P0 " { 0 })) = 0 by A2, Def1;

      (P0 " { 0 }) = {} by A12;

      then

       A13: ( Intersection (Fy,P0, 0 )) = ( union ( rng Fy)) by Th33;

      (XFS . 0 ) = ( card ( Intersection (Fy,P0, 0 ))) by A6, A7, A5, A10, A11;

      hence thesis by A8, A13, A9, AFINSQ_2: 51;

    end;

    theorem :: CARD_FIN:43



     Th42: ( dom Fy) = X & k > ( card X) implies ( Card_Intersection (Fy,k)) = 0

    proof

      assume that

       A1: ( dom Fy) = X and

       A2: k > ( card X);

      set Ch = ( Choose (X,k, 0 ,1));

      consider P be Function of ( card Ch), Ch such that

       A3: P is one-to-one by Lm2;

      consider XFS be XFinSequence of NAT such that

       A4: ( dom XFS) = ( dom P) and for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (Fy,f, 0 ))) and

       A5: ( Card_Intersection (Fy,k)) = ( Sum XFS) by A1, A3, Def3;

      Ch is empty by A2, Th9;

      then XFS = 0 by A4;

      hence thesis by A5;

    end;

    theorem :: CARD_FIN:44



     Th43: for Fy, X st ( dom Fy) = X holds for P be Function of ( card X), X st P is one-to-one holds ex XFS be XFinSequence of NAT st ( dom XFS) = ( card X) & (for z st z in ( dom XFS) holds (XFS . z) = ( card ((Fy * P) . z))) & ( Card_Intersection (Fy,1)) = ( Sum XFS)

    proof

      let Fy, X such that

       A1: ( dom Fy) = X;

      let P be Function of ( card X), X such that

       A2: P is one-to-one;

      per cases ;

        suppose

         A3: X = {} ;

        reconsider XFS = {} as XFinSequence;

        ( rng {} ) c= {} & {} c= NAT ;

        then

        reconsider XFS as XFinSequence of NAT by RELAT_1:def 19;

        take XFS;

        thus ( card X) = ( dom XFS) & for z st z in ( dom XFS) holds (XFS . z) = ( card ((Fy * P) . z)) by A3;

        ( Sum XFS) = 0 ;

        hence thesis by A1, A3, Th42, CARD_1: 27;

      end;

        suppose X <> {} ;

        then

        reconsider cX = ( card X) as non empty set;

        deffunc xfs( Element of cX) = ( card ((Fy * P) . $1));

        consider XFS be Function of cX, NAT such that

         A4: for x be Element of cX holds (XFS . x) = xfs(x) from FUNCT_2:sch 4;



         A5: ( dom XFS) = cX by FUNCT_2:def 1;

        then

        reconsider XFS as XFinSequence by AFINSQ_1: 5;

        reconsider XFS as XFinSequence of NAT ;

        take XFS;

        thus ( card X) = ( dom XFS) by FUNCT_2:def 1;

        thus for z st z in ( dom XFS) holds (XFS . z) = ( card ((Fy * P) . z)) by A4, A5;

        thus ( Card_Intersection (Fy,1)) = ( Sum XFS)

        proof

          deffunc p1( object) = (((P . $1) .--> 0 ) +* ((X \ {(P . $1)}) --> 1));



           A6: for x be object st x in cX holds p1(x) in ( Choose (X,1, 0 ,1))

          proof

            let x be object;

            assume x in cX;

            then x in ( dom P) by CARD_1: 27, FUNCT_2:def 1;

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

            then

             A7: ( {(P . x)} \/ (X \ {(P . x)})) = X by ZFMISC_1: 116;

             {(P . x)} misses (X \ {(P . x)}) & ( card {(P . x)}) = 1 by CARD_1: 30, XBOOLE_1: 79;

            hence thesis by A7, Th17;

          end;

          consider P1 be Function of cX, ( Choose (X,1, 0 ,1)) such that

           A8: for z be object st z in cX holds (P1 . z) = p1(z) from FUNCT_2:sch 2( A6);

          ( Choose (X,1, 0 ,1)) c= ( rng P1)

          proof

            ( card X) = ( card ( card X));

            then

             A9: P is onto by A2, FINSEQ_4: 63;

            let z be object;

            assume z in ( Choose (X,1, 0 ,1));

            then

            consider F be Function of X, { 0 , 1} such that

             A10: F = z and

             A11: ( card (F " { 0 })) = 1 by Def1;

            consider x1 be object such that

             A12: (F " { 0 }) = {x1} by A11, CARD_2: 42;



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

            then x1 in X by A12;

            then x1 in ( rng P) by A9, FUNCT_2:def 3;

            then

            consider x2 be object such that

             A14: x2 in ( dom P) and

             A15: (P . x2) = x1 by FUNCT_1:def 3;



             A16: (P1 . x2) = F

            proof

              set F1 = ((X \ {(P . x2)}) --> 1);

              set F0 = ((P . x2) .--> 0 );

              set P1x = (F0 +* F1);



               A17: ( {(P . x2)} \/ (X \ {(P . x2)})) = X by A12, A13, A15, ZFMISC_1: 116;

               A18:

              now

                let d be object such that

                 A19: d in ( dom F);

                now

                  per cases by A17, A19, XBOOLE_0:def 3;

                    suppose

                     A20: d in {(P . x2)};



                     A21: {(P . x2)} misses (X \ {(P . x2)}) by XBOOLE_1: 79;

                    ( dom F0) = {(P . x2)} & ( dom F1) = (X \ {(P . x2)});

                    then (P1x . d) = (F0 . d) by A20, A21, FUNCT_4: 16;

                    then

                     A22: (P1x . d) = 0 ;

                    (F . d) in { 0 } by A12, A15, A20, FUNCT_1:def 7;

                    hence (P1x . d) = (F . d) by A22, TARSKI:def 1;

                  end;

                    suppose

                     A23: d in (X \ {(P . x2)});

                    then d in ( dom F1);

                    then (P1x . d) = (F1 . d) by FUNCT_4: 13;

                    then

                     A24: (P1x . d) = 1 by A23, FUNCOP_1: 7;



                     A25: X = ( dom F) by FUNCT_2:def 1;

                     not d in {x1} by A15, A23, XBOOLE_0:def 5;

                    then not (F . d) in { 0 } by A12, A23, A25, FUNCT_1:def 7;

                    then

                     A26: not (F . d) = 0 by TARSKI:def 1;

                    (F . d) in ( rng F) by A23, A25, FUNCT_1:def 3;

                    hence (P1x . d) = (F . d) by A24, A26, TARSKI:def 2;

                  end;

                end;

                hence (P1x . d) = (F . d);

              end;



               A27: X = (( dom F0) \/ ( dom F1)) by A17;

              ( dom F) = X & ( dom P1x) = (( dom F0) \/ ( dom F1)) by FUNCT_2:def 1, FUNCT_4:def 1;

              then P1x = F by A27, A18;

              hence thesis by A8, A14;

            end;

            ( card ( Choose (X,1, 0 ,1))) = (( card X) choose 1) by Th15;

            then ( card ( Choose (X,1, 0 ,1))) = cX by NAT_1: 14, NEWTON: 23;

            then ( dom P1) = cX by CARD_1: 27, FUNCT_2:def 1;

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

          end;

          then

           A28: ( Choose (X,1, 0 ,1)) = ( rng P1);

          then

           A29: P1 is onto by FUNCT_2:def 3;

          ( card ( Choose (X,1, 0 ,1))) = (( card X) choose 1) by Th15;

          then

           A30: ( card X) = ( card ( Choose (X,1, 0 ,1))) by A28, NAT_1: 14, NEWTON: 23;

          then

          reconsider P1 as Function of ( card ( Choose (X,1, 0 ,1))), ( Choose (X,1, 0 ,1));

          ( card ( card X)) = ( card X);

          then P1 is one-to-one by A29, A30, FINSEQ_4: 63;

          then

          consider XFS1 be XFinSequence of NAT such that

           A31: ( dom XFS1) = ( dom P1) and

           A32: for z, f st z in ( dom XFS1) & f = (P1 . z) holds (XFS1 . z) = ( card ( Intersection (Fy,f, 0 ))) and

           A33: ( Card_Intersection (Fy,1)) = ( Sum XFS1) by A1, Def3;

          ( Choose (X,1, 0 ,1)) = {} implies ( card ( Choose (X,1, 0 ,1))) = {} ;

          then

           A34: ( dom P1) = ( card ( Choose (X,1, 0 ,1))) by FUNCT_2:def 1;



           A35: for z be object st z in ( dom XFS1) holds (XFS1 . z) = (XFS . z)

          proof

            let z be object such that

             A36: z in ( dom XFS1);

             p1(z) in ( Choose (X,1, 0 ,1)) by A6, A30, A31, A36;

            then

            consider f be Function of X, { 0 , 1} such that

             A37: f = p1(z) and

             A38: ( card (f " { 0 })) = 1 by Def1;

            consider x1 be object such that

             A39: (f " { 0 }) = {x1} by A38, CARD_2: 42;

            (P1 . z) = p1(z) by A8, A30, A31, A36;

            then

             A40: (XFS1 . z) = ( card ( Intersection (Fy,f, 0 ))) by A32, A36, A37;



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



             A43: (P . z) in {(P . z)} by TARSKI:def 1;



             A44: (P . z) in (( dom ((P . z) .--> 0 )) \/ ( dom ((X \ {(P . z)}) --> 1))) by A43, XBOOLE_0:def 3;

            ( not (P . z) in (X \ {(P . z)})) & (((P . z) .--> 0 ) . (P . z)) = 0 by A43, XBOOLE_0:def 5;

            then

             A45: ( p1(z) . (P . z)) = 0 by A44, FUNCT_4:def 1;

            (P . z) in ( dom p1(z)) by A44, FUNCT_4:def 1;

            then

             A46: (P . z) in (f " { 0 }) by A37, A45, A41, FUNCT_1:def 7;

            then (P . z) = x1 by A39, TARSKI:def 1;

            then

             A47: ( card ( Intersection (Fy,f, 0 ))) = ( card (Fy . (P . z))) by A39, Th34;



             A48: (XFS . z) = ( card ((Fy * P) . z)) by A4, A30, A31, A36;

            z in ( dom P) by A30, A31, A34, A36, A46, FUNCT_2:def 1;

            hence thesis by A47, A40, A48, FUNCT_1: 13;

          end;

          ( dom XFS1) = ( dom XFS) by A30, A31, A34, FUNCT_2:def 1;

          hence thesis by A33, A35, FUNCT_1:def 11;

        end;

      end;

    end;

    theorem :: CARD_FIN:45



     Th44: for x be object holds ( dom Fy) = X implies ( Card_Intersection (Fy,( card X))) = ( card ( Intersection (Fy,(X --> x),x)))

    proof

      let x be object;

      set Ch = ( Choose (X,( card X),x, {x}));

      consider P be Function of ( card Ch), Ch such that

       A1: P is one-to-one by Lm2;



       S: x in {x} by TARSKI:def 1;

      then

      reconsider x as set;

       not x in x;

      then

       A2: x <> {x} by S;

      assume ( dom Fy) = X;

      then

      consider XFS be XFinSequence of NAT such that

       A3: ( dom XFS) = ( dom P) and

       A4: (for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (Fy,f,x)))) & ( Card_Intersection (Fy,( card X))) = ( Sum XFS) by A1, A2, Def3;



       A5: ( card Ch) = 1 by Th11;

      then

      consider ch be object such that

       A6: Ch = {ch} by CARD_2: 42;

      x in {x} by TARSKI:def 1;

      then (X \/ {} ) = X & {x} <> x;

      then (( {} --> {x}) +* (X --> x)) in Ch by Th16;

      then ( {} +* (X --> x)) in Ch;

      then (X --> x) in Ch;

      then

       A7: (X --> x) = ch by A6, TARSKI:def 1;



       A8: Ch = {} implies ( card Ch) = {} ;

      then

       A9: ( dom P) = ( card Ch) by FUNCT_2:def 1;

      then 0 in ( dom P) by A5, CARD_1: 49, TARSKI:def 1;

      then (P . 0 ) in ( rng P) by FUNCT_1:def 3;

      then

       A10: (P . 0 ) = ch by A6, TARSKI:def 1;

      ( len XFS) = 1 by A3, A8, A5, FUNCT_2:def 1;

      then XFS = <%(XFS . 0 )%> by AFINSQ_1: 34;

      then ( addnat "**" XFS) = (XFS . 0 ) by AFINSQ_2: 37;

      then

       A11: ( Sum XFS) = (XFS . 0 ) by AFINSQ_2: 51;

       0 in ( dom XFS) by A3, A5, A9, CARD_1: 49, TARSKI:def 1;

      hence thesis by A4, A11, A10, A7;

    end;

    theorem :: CARD_FIN:46



     Th45: for x be object holds Fy = (x .--> X) implies ( Card_Intersection (Fy,1)) = ( card X)

    proof

      let x be object;

      assume

       A1: Fy = (x .--> X);

      then

       A2: ( dom Fy) = {x};



       A3: x in {x} by TARSKI:def 1;

      then

       A4: ((x .--> x) " {x}) = {x} by FUNCOP_1: 14;

      (Fy . x) = X by A1, A3, FUNCOP_1: 7;

      then 1 = ( card {x}) & ( Intersection (Fy,(x .--> x),x)) = X by A4, Th34, CARD_1: 30;

      hence thesis by A2, Th44;

    end;

    theorem :: CARD_FIN:47

    x <> y & Fy = ((x,y) --> (X,Y)) implies ( Card_Intersection (Fy,1)) = (( card X) + ( card Y)) & ( Card_Intersection (Fy,2)) = ( card (X /\ Y))

    proof

      assume that

       A1: x <> y and

       A2: Fy = ((x,y) --> (X,Y));

      set P = (( 0 ,1) --> (x,y));



       A3: ( dom P) = { 0 , 1} & ( rng P) = {x, y} by FUNCT_4: 62, FUNCT_4: 64;

      ( card {x, y}) = 2 by A1, CARD_2: 57;

      then

      reconsider P as Function of ( card {x, y}), {x, y} by A3, CARD_1: 50, FUNCT_2: 1;



       A4: ( card ( card {x, y})) = ( card {x, y});



       A5: (P . 0 ) = x & (Fy . x) = X by A1, A2, FUNCT_4: 63;



       A6: (P . 1) = y & (Fy . y) = Y by A2, FUNCT_4: 63;



       A7: ( dom Fy) = {x, y} by A2, FUNCT_4: 62;

      ( rng P) = {x, y} by FUNCT_4: 64;

      then P is onto by FUNCT_2:def 3;

      then P is one-to-one by A4, FINSEQ_4: 63;

      then

      consider XFS be XFinSequence of NAT such that

       A8: ( dom XFS) = ( card {x, y}) and

       A9: for z st z in ( dom XFS) holds (XFS . z) = ( card ((Fy * P) . z)) and

       A10: ( Card_Intersection (Fy,1)) = ( Sum XFS) by A7, Th43;

      ( len XFS) = 2 by A1, A8, CARD_2: 57;

      then

       A11: XFS = <%(XFS . 0 ), (XFS . 1)%> by AFINSQ_1: 38;



       A12: ( dom P) = { 0 , 1} by FUNCT_4: 62;

      then 1 in ( dom P) by TARSKI:def 2;

      then

       A13: ((Fy * P) . 1) = (Fy . (P . 1)) by FUNCT_1: 13;

       0 in { 0 } by TARSKI:def 1;

      then

       A14: (( {x, y} --> 0 ) " { 0 }) = {x, y} by FUNCOP_1: 14;

      (Fy . x) = X & (Fy . y) = Y by A1, A2, FUNCT_4: 63;

      then

       A15: ( Intersection (Fy,( {x, y} --> 0 ), 0 )) = (X /\ Y) by A14, Th35;

       0 in ( dom P) by A12, TARSKI:def 2;

      then

       A16: ((Fy * P) . 0 ) = (Fy . (P . 0 )) by FUNCT_1: 13;



       A17: ( dom XFS) = 2 by A1, A8, CARD_2: 57;

      then 1 in ( dom XFS) by CARD_1: 50, TARSKI:def 2;

      then

       A18: (XFS . 1) = ( card Y) by A9, A6, A13;

       0 in ( dom XFS) by A17, CARD_1: 50, TARSKI:def 2;

      then (XFS . 0 ) = ( card X) by A9, A5, A16;

      then ( addnat "**" XFS) = ( addnat . (( card X),( card Y))) by A11, A18, AFINSQ_2: 38;

      then

       A19: ( addnat "**" XFS) = (( card X) + ( card Y)) by BINOP_2:def 23;

      ( card {x, y}) = 2 & ( dom Fy) = {x, y} by A1, A2, CARD_2: 57, FUNCT_4: 62;

      hence thesis by A10, A19, A15, Th44, AFINSQ_2: 51;

    end;

    theorem :: CARD_FIN:48



     Th47: for Fy, x st ( dom Fy) is finite & x in ( dom Fy) holds ( Card_Intersection (Fy,1)) = (( Card_Intersection ((Fy | (( dom Fy) \ {x})),1)) + ( card (Fy . x)))

    proof

      let Fy, x such that

       A1: ( dom Fy) is finite and

       A2: x in ( dom Fy);

      reconsider X = ( dom Fy) as finite set by A1;

      ( card X) > 0 by A2;

      then

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

      set Xx = (X \ {x});



       A3: Xx = {} implies ( card Xx) = {} ;

      consider Px be Function of ( card Xx), Xx such that

       A4: Px is one-to-one by Lm2;

       not ( card Xx) in ( card Xx);

      then

      consider P be Function of (( card Xx) \/ {( card Xx)}), (Xx \/ {x}) such that

       A5: (P | ( card Xx)) = Px and

       A6: (P . ( card Xx)) = x by A3, STIRL2_1: 57;

       not x in Xx by ZFMISC_1: 56;

      then

       A7: P is one-to-one by A4, A3, A5, A6, STIRL2_1: 58;



       A8: ( card X) = ( Segm (k + 1));

      then

       A9: ( card Xx) = ( Segm k) by A2, STIRL2_1: 55;

      then ( card X) = (( card Xx) \/ {( card Xx)}) by A8, AFINSQ_1: 2;

      then

      reconsider P as Function of ( card X), X by A2, ZFMISC_1: 116;

      consider XFS be XFinSequence of NAT such that

       A10: ( dom XFS) = ( card X) and

       A11: for z st z in ( dom XFS) holds (XFS . z) = ( card ((Fy * P) . z)) and

       A12: ( Card_Intersection (Fy,1)) = ( Sum XFS) by A7, Th43;



       A13: (P . k) = x by A2, A6, A8, STIRL2_1: 55;

      (X /\ Xx) = Xx by XBOOLE_1: 28;

      then ( dom (Fy | Xx)) = Xx by RELAT_1: 61;

      then

      consider XFSx be XFinSequence of NAT such that

       A14: ( dom XFSx) = ( card Xx) and

       A15: for z st z in ( dom XFSx) holds (XFSx . z) = ( card (((Fy | Xx) * Px) . z)) and

       A16: ( Card_Intersection ((Fy | Xx),1)) = ( Sum XFSx) by A4, Th43;

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

      then

       A17: ( Segm k) c= ( Segm (k + 1)) by NAT_1: 39;



       A18: for y be object st y in ( dom XFSx) holds (XFS . y) = (XFSx . y)

      proof



         A19: Xx = (X /\ Xx) & (X /\ Xx) = ( dom (Fy | Xx)) by RELAT_1: 61, XBOOLE_1: 28;

        let y be object such that

         A20: y in ( dom XFSx);



         A21: (XFS . y) = ( card ((Fy * P) . y)) by A14, A9, A10, A11, A17, A20;



         A22: ( dom Px) = k by A3, A9, FUNCT_2:def 1;

        then (Px . y) in ( rng Px) by A14, A9, A20, FUNCT_1:def 3;

        then

         A23: ((Fy | Xx) . (Px . y)) = (Fy . (Px . y)) by A19, FUNCT_1: 47;

        ( dom P) = (k + 1) by CARD_1: 27, FUNCT_2:def 1;

        then

         A24: ((Fy * P) . y) = (Fy . (P . y)) by A14, A9, A17, A20, FUNCT_1: 13;

        (Px . y) = (P . y) by A14, A5, A9, A20, A22, FUNCT_1: 47;

        then ((Fy * P) . y) = (((Fy | Xx) * Px) . y) by A14, A9, A20, A22, A24, A23, FUNCT_1: 13;

        hence thesis by A15, A20, A21;

      end;

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

      then

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

      then k in ( dom P) by CARD_1: 27, FUNCT_2:def 1;

      then

       A26: ((Fy * P) . k) = (Fy . (P . k)) by FUNCT_1: 13;

      (( dom XFS) /\ k) = ( dom XFSx) by A14, A9, A10, A17, XBOOLE_1: 28;

      then (XFS | k) = XFSx by A18, FUNCT_1: 46;

      then

       A27: (( Sum XFSx) + (XFS . k)) = ( Sum (XFS | (k + 1))) by A10, A25, AFINSQ_2: 65;

      (XFS . k) = ( card ((Fy * P) . k)) by A10, A11, A25;

      hence thesis by A16, A10, A12, A27, A26, A13;

    end;

    theorem :: CARD_FIN:49



     Th48: ( dom ( Intersect (F,(( dom F) --> X9)))) = ( dom F) & for x st x in ( dom F) holds (( Intersect (F,(( dom F) --> X9))) . x) = ((F . x) /\ X9)

    proof



       A1: (( dom F) /\ ( dom (( dom F) --> X9))) = ( dom F);

      hence ( dom F) = ( dom ( Intersect (F,(( dom F) --> X9)))) by YELLOW20:def 2;

      let x;

      assume

       A2: x in ( dom F);

      then (( Intersect (F,(( dom F) --> X9))) . x) = ((F . x) /\ ((( dom F) --> X9) . x)) by A1, YELLOW20:def 2;

      hence thesis by A2, FUNCOP_1: 7;

    end;

    theorem :: CARD_FIN:50



     Th49: (( union ( rng F)) /\ X9) = ( union ( rng ( Intersect (F,(( dom F) --> X9)))))

    proof

      set I = ( Intersect (F,(( dom F) --> X9)));

      thus (( union ( rng F)) /\ X9) c= ( union ( rng I))

      proof

        let x be object such that

         A1: x in (( union ( rng F)) /\ X9);



         A2: x in X9 by A1, XBOOLE_0:def 4;

        x in ( union ( rng F)) by A1, XBOOLE_0:def 4;

        then

        consider Fx be set such that

         A3: x in Fx and

         A4: Fx in ( rng F) by TARSKI:def 4;

        consider x1 be object such that

         A5: x1 in ( dom F) and

         A6: (F . x1) = Fx by A4, FUNCT_1:def 3;

        x1 in ( dom I) by A5, Th48;

        then

         A7: (I . x1) in ( rng I) by FUNCT_1:def 3;

        (I . x1) = (Fx /\ X9) by A5, A6, Th48;

        then x in (I . x1) by A3, A2, XBOOLE_0:def 4;

        hence thesis by A7, TARSKI:def 4;

      end;

      thus ( union ( rng I)) c= (( union ( rng F)) /\ X9)

      proof

        let x be object;

        assume x in ( union ( rng I));

        then

        consider Ix be set such that

         A8: x in Ix and

         A9: Ix in ( rng I) by TARSKI:def 4;

        consider x1 be object such that

         A10: x1 in ( dom I) and

         A11: (I . x1) = Ix by A9, FUNCT_1:def 3;



         A12: x1 in ( dom F) by A10, Th48;

        then

         A13: (F . x1) in ( rng F) by FUNCT_1:def 3;



         A14: (I . x1) = ((F . x1) /\ X9) by A12, Th48;

        then x in (F . x1) by A8, A11, XBOOLE_0:def 4;

        then

         A15: x in ( union ( rng F)) by A13, TARSKI:def 4;

        x in X9 by A8, A11, A14, XBOOLE_0:def 4;

        hence thesis by A15, XBOOLE_0:def 4;

      end;

    end;

    theorem :: CARD_FIN:51



     Th50: (( Intersection (F,Ch,y)) /\ X9) = ( Intersection (( Intersect (F,(( dom F) --> X9))),Ch,y))

    proof

      set I = ( Intersect (F,(( dom F) --> X9)));

      set Int1 = ( Intersection (F,Ch,y));

      set Int2 = ( Intersection (I,Ch,y));

      thus (Int1 /\ X9) c= Int2

      proof

        let x be object such that

         A1: x in (Int1 /\ X9);



         A2: for z st z in ( dom Ch) & (Ch . z) = y holds x in (I . z)

        proof



           A3: x in Int1 by A1, XBOOLE_0:def 4;

          let z;

          assume z in ( dom Ch) & (Ch . z) = y;

          then

           A4: x in (F . z) by A3, Def2;

          then

           A5: z in ( dom F) by FUNCT_1:def 2;

          x in X9 by A1, XBOOLE_0:def 4;

          then x in ((F . z) /\ X9) by A4, XBOOLE_0:def 4;

          hence thesis by A5, Th48;

        end;

        x in X9 by A1, XBOOLE_0:def 4;

        then x in (( union ( rng F)) /\ X9) by A1, XBOOLE_0:def 4;

        then x in ( union ( rng I)) by Th49;

        hence thesis by A2, Def2;

      end;

      thus Int2 c= (Int1 /\ X9)

      proof

        let x be object such that

         A6: x in Int2;

        x in ( union ( rng I)) by A6;

        then

         A7: x in (( union ( rng F)) /\ X9) by Th49;

        then

         A8: x in X9 by XBOOLE_0:def 4;



         A9: for z st z in ( dom Ch) & (Ch . z) = y holds x in (F . z)

        proof



           A10: ( dom I) = ( dom F) by Th48;

          let z;

          assume z in ( dom Ch) & (Ch . z) = y;

          then

           A11: x in (I . z) by A6, Def2;

          then z in ( dom I) by FUNCT_1:def 2;

          then x in ((F . z) /\ X9) by A11, A10, Th48;

          hence thesis by XBOOLE_0:def 4;

        end;

        x in ( union ( rng F)) by A7, XBOOLE_0:def 4;

        then x in Int1 by A9, Def2;

        hence thesis by A8, XBOOLE_0:def 4;

      end;

    end;

    theorem :: CARD_FIN:52



     Th51: for F,G be XFinSequence st F is one-to-one & G is one-to-one & ( rng F) misses ( rng G) holds (F ^ G) is one-to-one

    proof

      let F,G be XFinSequence such that

       A1: F is one-to-one and

       A2: G is one-to-one and

       A3: ( rng F) misses ( rng G);

      (( len F),( rng F)) are_equipotent by A1, WELLORD2:def 4;

      then

       A4: ( card ( len F)) = ( card ( rng F)) by CARD_1: 5;

      (( len G),( rng G)) are_equipotent by A2, WELLORD2:def 4;

      then

       A5: ( card ( len G)) = ( card ( rng G)) by CARD_1: 5;

      reconsider FG = (F ^ G) as Function of ( dom (F ^ G)), ( rng (F ^ G)) by FUNCT_2: 1;



       A6: ( dom (F ^ G)) = (( len F) + ( len G)) by AFINSQ_1:def 3;



       A7: FG is onto by FUNCT_2:def 3;

      ( card (( rng F) \/ ( rng G))) = (( card ( rng F)) + ( card ( rng G))) by A3, CARD_2: 40;

      then ( card ( dom (F ^ G))) = ( card ( rng (F ^ G))) by A4, A5, A6, AFINSQ_1: 26;

      hence thesis by A7, FINSEQ_4: 63;

    end;

    theorem :: CARD_FIN:53



     Th52: for Fy, X, x, n st ( dom Fy) = X & x in ( dom Fy) & k > 0 holds ( Card_Intersection (Fy,(k + 1))) = (( Card_Intersection ((Fy | (( dom Fy) \ {x})),(k + 1))) + ( Card_Intersection (( Intersect ((Fy | (( dom Fy) \ {x})),((( dom Fy) \ {x}) --> (Fy . x)))),k)))

    proof

      let Fy, X, x, n such that

       A1: ( dom Fy) = X and

       A2: x in ( dom Fy) and

       A3: k > 0 ;

      set Xx = (X \ {x});



       A4: (Xx \/ {x}) = X by A1, A2, ZFMISC_1: 116;

      set I = ( Intersect ((Fy | (( dom Fy) \ {x})),((( dom Fy) \ {x}) --> (Fy . x))));

      set X1 = { f where f be Function of (Xx \/ {x}), {1, 0 } : ( card (f " {1})) = (k + 1) & (f . x) = 1 };

      set X0 = { f where f be Function of (Xx \/ {x}), {1, 0 } : ( card (f " {1})) = (k + 1) & (f . x) = 0 };

      (X0 \/ X1) = ( Choose ((Xx \/ {x}),(k + 1),1, 0 )) by Lm1;

      then

      reconsider X0, X1 as finite set by FINSET_1: 1, XBOOLE_1: 7;

      consider P1 be Function of ( card X1), X1 such that

       A5: P1 is one-to-one by Lm2;

       not x in Xx by ZFMISC_1: 56;

      then

       A6: ( card ( Choose (Xx,k,1, 0 ))) = ( card X1) by Th12;

      defpred p1[ object, object] means ex f st f = (P1 . $1) & f in X1 & $2 = (f | Xx);



       A7: for x1 be object st x1 in ( card X1) holds ex P1x1 be object st P1x1 in ( Choose (Xx,k,1, 0 )) & p1[x1, P1x1]

      proof

         not x in Xx by ZFMISC_1: 56;

        then

         A8: ((Xx \/ {x}) \ {x}) = Xx by ZFMISC_1: 117;

        let x1 be object;

        assume x1 in ( card X1);

        then x1 in ( dom P1) by CARD_1: 27, FUNCT_2:def 1;

        then

         A9: (P1 . x1) in ( rng P1) by FUNCT_1:def 3;

        then (P1 . x1) in X1;

        then

        consider P1x1 be Function of (Xx \/ {x}), {1, 0 } such that

         A10: (P1 . x1) = P1x1 and

         A11: ( card (P1x1 " {1})) = (k + 1) and

         A12: (P1x1 . x) = 1;



         A13: ( dom P1x1) = (Xx \/ {x}) by FUNCT_2:def 1;



         A14: ( rng (P1x1 | Xx)) c= {1, 0 };

        ((Xx \/ {x}) /\ Xx) = Xx by XBOOLE_1: 7, XBOOLE_1: 28;

        then ( dom (P1x1 | Xx)) = Xx by A13, RELAT_1: 61;

        then

        reconsider Px = (P1x1 | Xx) as Function of Xx, {1, 0 } by A14, FUNCT_2: 2;



         A15: not x in (Px " {1}) by ZFMISC_1: 56;

        x in {x} & ( dom P1x1) = (Xx \/ {x}) by FUNCT_2:def 1, TARSKI:def 1;

        then x in ( dom P1x1) by XBOOLE_0:def 3;

        then (P1x1 " {1}) = ((Px " {1}) \/ {x}) by A12, A13, A8, AFINSQ_2: 66;

        then (k + 1) = (( card (Px " {1})) + 1) by A11, A15, CARD_2: 41;

        then Px in ( Choose (Xx,k,1, 0 )) by Def1;

        hence thesis by A9, A10;

      end;

      consider P1x be Function of ( card X1), ( Choose (Xx,k,1, 0 )) such that

       A16: for x1 be object st x1 in ( card X1) holds p1[x1, (P1x . x1)] from FUNCT_2:sch 1( A7);

      for x1,x2 be object st x1 in ( dom P1x) & x2 in ( dom P1x) & (P1x . x1) = (P1x . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         A17: x1 in ( dom P1x) and

         A18: x2 in ( dom P1x) and

         A19: (P1x . x1) = (P1x . x2);

        consider f2 be Function such that

         A20: f2 = (P1 . x2) and

         A21: f2 in X1 and

         A22: (P1x . x2) = (f2 | Xx) by A16, A18;

        consider f1 be Function such that

         A23: f1 = (P1 . x1) and

         A24: f1 in X1 and

         A25: (P1x . x1) = (f1 | Xx) by A16, A17;



         A26: ex F be Function of (Xx \/ {x}), {1, 0 } st f1 = F & ( card (F " {1})) = (k + 1) & (F . x) = 1 by A24;

        then

         A27: ( dom f1) = (Xx \/ {x}) by FUNCT_2:def 1;



         A28: ex F be Function of (Xx \/ {x}), {1, 0 } st f2 = F & ( card (F " {1})) = (k + 1) & (F . x) = 1 by A21;

        then

         A29: ( dom f2) = (Xx \/ {x}) by FUNCT_2:def 1;

        for z be object st z in ( dom f1) holds (f1 . z) = (f2 . z)

        proof

          let z be object such that

           A30: z in ( dom f1);

          now

            per cases by A27, A30, XBOOLE_0:def 3;

              suppose

               A31: z in Xx;

              then z in (( dom f1) /\ Xx) by A30, XBOOLE_0:def 4;

              then

               A32: ((f1 | Xx) . z) = (f1 . z) by FUNCT_1: 48;

              z in (( dom f2) /\ Xx) by A27, A29, A30, A31, XBOOLE_0:def 4;

              hence thesis by A19, A25, A22, A32, FUNCT_1: 48;

            end;

              suppose z in {x};

              then z = x by TARSKI:def 1;

              hence thesis by A26, A28;

            end;

          end;

          hence thesis;

        end;

        then

         A33: f1 = f2 by A27, A29;

        X1 = {} implies ( card X1) = {} ;

        then ( dom P1) = ( card X1) by FUNCT_2:def 1;

        hence thesis by A5, A17, A18, A23, A20, A33;

      end;

      then

       A34: P1x is one-to-one;

      (Xx /\ X) = Xx by XBOOLE_1: 28;

      then

       A35: ( dom (Fy | (( dom Fy) \ {x}))) = Xx by A1, RELAT_1: 61;

      then ( dom I) = Xx by A1, Th48;

      then

      consider XFS1 be XFinSequence of NAT such that

       A36: ( dom XFS1) = ( dom P1x) and

       A37: for z, f st z in ( dom XFS1) & f = (P1x . z) holds (XFS1 . z) = ( card ( Intersection (I,f,1))) and

       A38: ( Card_Intersection (I,k)) = ( Sum XFS1) by A6, A34, Def3;



       A39: ( addnat "**" XFS1) = ( Card_Intersection (I,k)) by A38, AFINSQ_2: 51;

       not x in Xx by ZFMISC_1: 56;

      then

       A40: ( card ( Choose (Xx,(k + 1),1, 0 ))) = ( card X0) by Th13;

      set Ch = ( Choose (X,(k + 1),1, 0 ));

      consider P0 be Function of ( card X0), X0 such that

       A41: P0 is one-to-one by Lm2;



       A42: X1 = {} implies ( card X1) = {} ;

      then

       A43: ( dom P1) = ( card X1) by FUNCT_2:def 1;



       A44: X0 = {} implies ( card X0) = {} ;

      then ( dom P0) = ( card X0) by FUNCT_2:def 1;

      then

      reconsider XP0 = P0, XP1 = P1 as XFinSequence by A43, AFINSQ_1: 5;



       A45: ( card X0) = ( len XP0) by A44, FUNCT_2:def 1;

      defpred p0[ object, object] means ex f st f = (P0 . $1) & f in X0 & $2 = (f | Xx);



       A46: for x0 be object st x0 in ( card X0) holds ex P0x0 be object st P0x0 in ( Choose (Xx,(k + 1),1, 0 )) & p0[x0, P0x0]

      proof

        let x0 be object;

        assume x0 in ( card X0);

        then x0 in ( dom P0) by CARD_1: 27, FUNCT_2:def 1;

        then

         A47: (P0 . x0) in ( rng P0) by FUNCT_1:def 3;

        then (P0 . x0) in X0;

        then

        consider P0x0 be Function of (Xx \/ {x}), {1, 0 } such that

         A48: (P0 . x0) = P0x0 and

         A49: ( card (P0x0 " {1})) = (k + 1) and

         A50: (P0x0 . x) = 0 ;



         A51: ( dom P0x0) = (Xx \/ {x}) by FUNCT_2:def 1;



         A52: ( rng (P0x0 | Xx)) c= {1, 0 };

        ((Xx \/ {x}) /\ Xx) = Xx by XBOOLE_1: 7, XBOOLE_1: 28;

        then ( dom (P0x0 | Xx)) = Xx by A51, RELAT_1: 61;

        then

        reconsider Px = (P0x0 | Xx) as Function of Xx, {1, 0 } by A52, FUNCT_2: 2;

         not x in Xx by ZFMISC_1: 56;

        then ((Xx \/ {x}) \ {x}) = Xx by ZFMISC_1: 117;

        then (P0x0 " {1}) = (Px " {1}) by A50, A51, AFINSQ_2: 67;

        then Px in ( Choose (Xx,(k + 1),1, 0 )) by A49, Def1;

        hence thesis by A47, A48;

      end;

      consider P0x be Function of ( card X0), ( Choose (Xx,(k + 1),1, 0 )) such that

       A53: for x1 be object st x1 in ( card X0) holds p0[x1, (P0x . x1)] from FUNCT_2:sch 1( A46);

      (( rng P0) \/ ( rng P1)) c= (X0 \/ X1) by XBOOLE_1: 13;

      then ( rng (XP0 ^ XP1)) c= (X0 \/ X1) by AFINSQ_1: 26;

      then

       A54: ( rng (XP0 ^ XP1)) c= Ch by A4, Lm1;



       A55: ( card X1) = ( len XP1) by A42, FUNCT_2:def 1;

      for x1,x2 be object st x1 in ( dom P0x) & x2 in ( dom P0x) & (P0x . x1) = (P0x . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         A56: x1 in ( dom P0x) and

         A57: x2 in ( dom P0x) and

         A58: (P0x . x1) = (P0x . x2);

        consider f2 be Function such that

         A59: f2 = (P0 . x2) and

         A60: f2 in X0 and

         A61: (P0x . x2) = (f2 | Xx) by A53, A57;

        consider f1 be Function such that

         A62: f1 = (P0 . x1) and

         A63: f1 in X0 and

         A64: (P0x . x1) = (f1 | Xx) by A53, A56;



         A65: ex F be Function of (Xx \/ {x}), {1, 0 } st f1 = F & ( card (F " {1})) = (k + 1) & (F . x) = 0 by A63;

        then

         A66: ( dom f1) = (Xx \/ {x}) by FUNCT_2:def 1;



         A67: ex F be Function of (Xx \/ {x}), {1, 0 } st f2 = F & ( card (F " {1})) = (k + 1) & (F . x) = 0 by A60;

        then

         A68: ( dom f2) = (Xx \/ {x}) by FUNCT_2:def 1;

        for z be object st z in ( dom f1) holds (f1 . z) = (f2 . z)

        proof

          let z be object such that

           A69: z in ( dom f1);

          now

            per cases by A66, A69, XBOOLE_0:def 3;

              suppose

               A70: z in Xx;

              then z in (( dom f1) /\ Xx) by A69, XBOOLE_0:def 4;

              then

               A71: ((f1 | Xx) . z) = (f1 . z) by FUNCT_1: 48;

              z in (( dom f2) /\ Xx) by A66, A68, A69, A70, XBOOLE_0:def 4;

              hence thesis by A58, A64, A61, A71, FUNCT_1: 48;

            end;

              suppose z in {x};

              then z = x by TARSKI:def 1;

              hence thesis by A65, A67;

            end;

          end;

          hence thesis;

        end;

        then

         A72: f1 = f2 by A66, A68;

        X0 = {} implies ( card X0) = {} ;

        then ( dom P0) = ( card X0) by FUNCT_2:def 1;

        hence thesis by A41, A56, A57, A62, A59, A72;

      end;

      then P0x is one-to-one;

      then

      consider XFS0 be XFinSequence of NAT such that

       A73: ( dom XFS0) = ( dom P0x) and

       A74: for z, f st z in ( dom XFS0) & f = (P0x . z) holds (XFS0 . z) = ( card ( Intersection ((Fy | (( dom Fy) \ {x})),f,1))) and

       A75: ( Card_Intersection ((Fy | (( dom Fy) \ {x})),(k + 1))) = ( Sum XFS0) by A40, A35, Def3;

      ( Choose (Xx,(k + 1),1, 0 )) = {} implies ( card ( Choose (Xx,(k + 1),1, 0 ))) = {} ;

      then

       A76: ( dom P0x) = ( card X0) by A40, FUNCT_2:def 1;

       not x in Xx by ZFMISC_1: 56;

      then (( card X0) + ( card X1)) = ( card Ch) by A40, A6, A4, Th14;

      then ( dom (XP0 ^ XP1)) = ( card Ch) by A45, A55, AFINSQ_1:def 3;

      then

      reconsider XP01 = (XP0 ^ XP1) as Function of ( card Ch), Ch by A54, FUNCT_2: 2;

      ( rng P0) misses ( rng P1) by Lm1, XBOOLE_1: 64;

      then XP01 is one-to-one by A41, A5, Th51;

      then

      consider XFS be XFinSequence of NAT such that

       A77: ( dom XFS) = ( dom XP01) and

       A78: for z, f st z in ( dom XFS) & f = (XP01 . z) holds (XFS . z) = ( card ( Intersection (Fy,f,1))) and

       A79: ( Card_Intersection (Fy,(k + 1))) = ( Sum XFS) by A1, Def3;



       A80: ( addnat "**" XFS) = ( Card_Intersection (Fy,(k + 1))) by A79, AFINSQ_2: 51;

      ( Choose (Xx,k,1, 0 )) = {} implies ( card ( Choose (Xx,k,1, 0 ))) = {} ;

      then

       A81: ( dom P1x) = ( card X1) by A6, FUNCT_2:def 1;



       A82: for n be Nat st n in ( dom XFS0) holds (XFS . n) = (XFS0 . n)

      proof

        let n be Nat such that

         A83: n in ( dom XFS0);

        consider fx be Function such that

         A84: fx = (P0 . n) and

         A85: fx in X0 and

         A86: (P0x . n) = (fx | Xx) by A53, A73, A83;



         A87: (XFS0 . n) = ( card ( Intersection ((Fy | Xx),(fx | Xx),1))) by A1, A74, A83, A86;



         A88: ex fx9 be Function of (Xx \/ {x}), {1, 0 } st fx = fx9 & ( card (fx9 " {1})) = (k + 1) & (fx9 . x) = 0 by A85;

        then

        consider x1 be object such that

         A89: x1 in (fx " {1}) by CARD_1: 27, XBOOLE_0:def 1;

        (fx . x1) in {1} by A89, FUNCT_1:def 7;

        then

         A90: (fx . x1) = 1 by TARSKI:def 1;

        x1 in ( dom fx) by A89, FUNCT_1:def 7;

        then

         A91: 1 in ( rng fx) by A90, FUNCT_1:def 3;



         A92: (Xx \/ {x}) = X by A1, A2, ZFMISC_1: 116;



         A93: (( dom XFS0) + 0 qua Nat) <= (( dom XFS0) + ( dom XFS1)) by XREAL_1: 7;

        ( dom fx) = (Xx \/ {x}) by A88, FUNCT_2:def 1;

        then

         A94: (fx " {1}) = ((fx | Xx) " {1}) by A88, A92, AFINSQ_2: 67;

        n < ( len XFS0) by A83, AFINSQ_1: 86;

        then n < (( len XFS0) + ( dom XFS1)) by A93, XXREAL_0: 2;

        then n < ( len XFS) by A73, A36, A45, A55, A77, A76, A81, AFINSQ_1:def 3;

        then

         A95: n in ( dom XFS) by AFINSQ_1: 86;

        (XP01 . n) = (XP0 . n) by A73, A45, A83, AFINSQ_1:def 3;

        then

         A96: (XFS . n) = ( card ( Intersection (Fy,fx,1))) by A78, A84, A95;

        ((fx | Xx) " {1}) c= ( dom (fx | Xx)) & ( dom (fx | Xx)) c= Xx by RELAT_1: 58, RELAT_1: 132;

        then ( Intersection ((Fy | Xx),fx,1)) = ( Intersection (Fy,fx,1)) by A94, A91, Th29, XBOOLE_1: 1;

        hence thesis by A94, A96, A87, Th27;

      end;

      X1 = {} implies ( card X1) = {} ;

      then

       A97: ( dom P1) = ( card X1) by FUNCT_2:def 1;



       A98: for n be Nat st n in ( dom XFS1) holds (XFS . (( len XFS0) + n)) = (XFS1 . n)

      proof



         A99: (Xx \/ {x}) = X by A1, A2, ZFMISC_1: 116;

        let n be Nat such that

         A100: n in ( dom XFS1);

        consider fx be Function such that

         A101: fx = (P1 . n) and

         A102: fx in X1 and

         A103: (P1x . n) = (fx | Xx) by A16, A36, A100;

        consider fx9 be Function of (Xx \/ {x}), {1, 0 } such that

         A104: fx = fx9 and

         A105: ( card (fx9 " {1})) = (k + 1) and

         A106: (fx9 . x) = 1 by A102;



         A107: ( Intersection (( Intersect ((Fy | Xx),(Xx --> (Fy . x)))),(fx | Xx),1)) = (( Intersection ((Fy | Xx),(fx | Xx),1)) /\ (Fy . x)) by A1, A35, Th50;



         A108: ( dom fx9) = (Xx \/ {x}) by FUNCT_2:def 1;

        then

         A109: ( dom fx) = X by A1, A2, A104, ZFMISC_1: 116;



         A110: 1 in ( rng (fx | Xx)) & ((fx | Xx) " {1}) c= Xx

        proof



           A111: ((fx | Xx) " {1}) c= ( dom (fx | Xx)) & ( dom (fx | Xx)) = (( dom fx) /\ Xx) by RELAT_1: 61, RELAT_1: 132;

          reconsider fx1 = ((fx | Xx) " {1}) as finite set;

           not x in Xx by ZFMISC_1: 56;

          then not x in (( dom fx) /\ Xx) by XBOOLE_0:def 4;

          then not x in ( dom (fx | Xx)) by RELAT_1: 61;

          then

           A112: not x in fx1 by FUNCT_1:def 7;

          ( {x} \/ fx1) = (fx " {1}) by A1, A2, A104, A106, A109, AFINSQ_2: 66;

          then (( card fx1) + 1) = (k + 1) by A104, A105, A112, CARD_2: 41;

          then

          consider y be object such that

           A113: y in fx1 by A3, CARD_1: 27, XBOOLE_0:def 1;

          y in ( dom (fx | Xx)) by A113, FUNCT_1:def 7;

          then

           A114: ((fx | Xx) . y) in ( rng (fx | Xx)) by FUNCT_1:def 3;

          (( dom fx) /\ Xx) c= Xx & ((fx | Xx) . y) in {1} by A113, FUNCT_1:def 7, XBOOLE_1: 17;

          hence thesis by A111, A114, TARSKI:def 1;

        end;

        n < ( len XFS1) by A100, AFINSQ_1: 86;

        then (( len XFS0) + n) < (( dom XFS0) + ( dom XFS1)) by XREAL_1: 8;

        then (( dom XFS0) + n) < ( len XFS) by A73, A36, A45, A55, A77, A76, A81, AFINSQ_1:def 3;

        then

         A115: (( dom XFS0) + n) in ( dom XFS) by AFINSQ_1: 86;

        (XP01 . (n + ( len XP0))) = fx by A36, A97, A100, A101, AFINSQ_1:def 3;

        then

         A116: (XFS . (( dom XFS0) + n)) = ( card ( Intersection (Fy,fx,1))) by A73, A45, A78, A76, A115;

        (fx . x) in {1} by A104, A106, TARSKI:def 1;

        then

         A117: x in (fx " {1}) by A1, A2, A104, A108, A99, FUNCT_1:def 7;

        (XFS1 . n) = ( card ( Intersection (( Intersect ((Fy | Xx),(Xx --> (Fy . x)))),(fx | Xx),1))) by A1, A37, A100, A103;

        then (XFS1 . n) = ( card (( Intersection (Fy,(fx | Xx),1)) /\ (Fy . x))) by A110, A107, Th29;

        hence thesis by A117, A109, A116, Th31;

      end;

      ( dom XFS) = (( len XFS0) + ( len XFS1)) by A73, A36, A45, A55, A77, A76, A81, AFINSQ_1:def 3;

      then XFS = (XFS0 ^ XFS1) by A82, A98, AFINSQ_1:def 3;

      then

       A118: ( addnat "**" XFS) = ( addnat . (( addnat "**" XFS0),( addnat "**" XFS1))) by AFINSQ_2: 42;

      ( addnat "**" XFS0) = ( Card_Intersection ((Fy | (( dom Fy) \ {x})),(k + 1))) by A75, AFINSQ_2: 51;

      hence thesis by A118, A39, A80, BINOP_2:def 23;

    end;

    theorem :: CARD_FIN:54



     Th53: x in ( dom F) implies ( union ( rng F)) = (( union ( rng (F | (( dom F) \ {x})))) \/ (F . x))

    proof

      set d = (( dom F) \ {x});

      set Fd = (F | d);



       A1: (F | ( dom F)) = F;

      assume

       A2: x in ( dom F);

      then (d \/ {x}) = ( dom F) by ZFMISC_1: 116;

      then F = (Fd \/ (F | {x})) by A1, RELAT_1: 78;

      then

       A3: ( rng F) = (( rng Fd) \/ ( rng (F | {x}))) by RELAT_1: 12;

      ( Im (F,x)) = {(F . x)} by A2, FUNCT_1: 59;

      then ( rng (F | {x})) = {(F . x)} by RELAT_1: 115;

      then ( union ( rng F)) = (( union ( rng Fd)) \/ ( union {(F . x)})) by A3, ZFMISC_1: 78;

      hence thesis by ZFMISC_1: 25;

    end;

    theorem :: CARD_FIN:55



     Th54: for Fy be finite-yielding Function, X holds ex XFS be XFinSequence of INT st ( dom XFS) = ( card X) & for n st n in ( dom XFS) holds (XFS . n) = ((( - 1) |^ n) * ( Card_Intersection (Fy,(n + 1))))

    proof

      let Fy be finite-yielding Function, X;

      defpred P[ set, set] means for n st n = $1 holds $2 = ((( - 1) |^ n) * ( Card_Intersection (Fy,(n + 1))));



       A1: for k st k in ( Segm ( card X)) holds ex x be Element of INT st P[k, x]

      proof

        let k such that k in ( Segm ( card X));

        reconsider C = ((( - 1) |^ k) * ( Card_Intersection (Fy,(k + 1)))) as Element of INT by INT_1:def 2;

        take C;

        thus thesis;

      end;

      consider XFS be XFinSequence of INT such that

       A2: ( dom XFS) = ( Segm ( card X)) & for k st k in ( Segm ( card X)) holds P[k, (XFS . k)] from STIRL2_1:sch 5( A1);

      take XFS;

      thus thesis by A2;

    end;

    ::$Notion-Name

    theorem :: CARD_FIN:56



     Th55: for Fy be finite-yielding Function, X st ( dom Fy) = X holds for XFS be XFinSequence of INT st ( dom XFS) = ( card X) & for n st n in ( dom XFS) holds (XFS . n) = ((( - 1) |^ n) * ( Card_Intersection (Fy,(n + 1)))) holds ( card ( union ( rng Fy))) = ( Sum XFS)

    proof

      defpred P[ Nat] means for Fy be finite-yielding Function, X st ( dom Fy) = X & ( card X) = $1 holds for XFS be XFinSequence of INT st ( dom XFS) = ( card X) & for n st n in ( dom XFS) holds (XFS . n) = ((( - 1) |^ n) * ( Card_Intersection (Fy,(n + 1)))) holds ( card ( union ( rng Fy))) = ( Sum XFS);



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

      proof

        let k such that

         A2: P[k];

        let Fy be finite-yielding Function, X such that

         A3: ( dom Fy) = X and

         A4: ( card X) = (k + 1);

        ( rng Fy) is finite & for x st x in ( rng Fy) holds x is finite by A3, FINSET_1: 8;

        then

        reconsider urngFy = ( union ( rng Fy)) as finite set;

        let XFS be XFinSequence of INT such that

         A5: ( dom XFS) = ( card X) and

         A6: for n st n in ( dom XFS) holds (XFS . n) = ((( - 1) |^ n) * ( Card_Intersection (Fy,(n + 1))));

        per cases ;

          suppose

           A7: k = 0 ;

          then ( len XFS) = 1 by A4, A5;

          then

           A8: XFS = <%(XFS . 0 )%> by AFINSQ_1: 34;

          (XFS . 0 ) is Element of INT by INT_1:def 2;

          then

           A9: ( addint "**" XFS) = (XFS . 0 ) by A8, AFINSQ_2: 37;

           0 in ( dom XFS) by A4, A5, A7, CARD_1: 49, TARSKI:def 1;

          then

           A10: (XFS . 0 ) = ((( - 1) |^ 0 ) * ( Card_Intersection (Fy,( 0 qua Nat + 1)))) by A6;

          consider x be object such that

           A11: ( dom Fy) = {x} by A3, A4, A7, CARD_2: 42;



           A12: ( rng Fy) = {(Fy . x)} by A11, FUNCT_1: 4;

          then

           A13: ( union ( rng Fy)) = (Fy . x) by ZFMISC_1: 25;

          (( - 1) |^ 0 ) = 1 & Fy = (x .--> (Fy . x)) by A11, A12, FUNCOP_1: 9, NEWTON: 4;

          then (XFS . 0 ) = ( card ( union ( rng Fy))) by Th45, A13, A10;

          hence thesis by A9, AFINSQ_2: 50;

        end;

          suppose

           A14: k > 0 ;

          consider x be object such that

           A15: x in ( dom Fy) by A3, A4, CARD_1: 27, XBOOLE_0:def 1;

          reconsider x as set by TARSKI: 1;

          set Xx = (X \ {x});



           A16: ( card Xx) = k by A3, A4, A15, STIRL2_1: 55;

          set FyX = (Fy | Xx);

          reconsider urngFyX = ( union ( rng FyX)) as finite set;

          set Fyx = (Fy . x);

          set I = ( Intersect (FyX,(( dom FyX) --> (Fy . x))));

          consider XFyX be XFinSequence of INT such that

           A17: ( dom XFyX) = ( card Xx) and

           A18: for n st n in ( dom XFyX) holds (XFyX . n) = ((( - 1) |^ n) * ( Card_Intersection (FyX,(n + 1)))) by Th54;

          (urngFyX /\ (Fy . x)) = ( union ( rng I)) by Th49;

          then

          reconsider urngI = ( union ( rng I)) as finite set;

          consider XI be XFinSequence of INT such that

           A19: ( dom XI) = ( card Xx) and

           A20: for n st n in ( dom XI) holds (XI . n) = ((( - 1) |^ n) * ( Card_Intersection (I,(n + 1)))) by Th54;

          set XI1 = (( - 1) (#) XI);

          reconsider XI1 as XFinSequence of INT ;

          reconsider XcF = <%( card Fyx)%>, X0 = <% 0 %> as XFinSequence of INT ;

          reconsider F1 = ( <%( card Fyx)%> ^ XI1), F2 = (XFyX ^ <% 0 %>) as XFinSequence of INT ;



           A21: ( card Xx) = k by A3, A4, A15, STIRL2_1: 55;

          reconsider zz = 0 as Element of INT by INT_1:def 2;



           A22: ( addint "**" X0) = zz by AFINSQ_2: 37;

          ( card Fyx) is Element of INT by INT_1:def 2;

          then

           A23: ( addint "**" XcF) = ( card Fyx) by AFINSQ_2: 37;



           A24: (( - 1) * ( Sum XI)) = ( Sum XI1) by AFINSQ_2: 64;



           A25: ( addint "**" F1) = ( addint . (( card Fyx),( addint "**" XI1))) by A23, AFINSQ_2: 42

          .= (( card Fyx) + ( addint "**" XI1)) by BINOP_2:def 20

          .= (( card Fyx) + ( Sum XI1)) by AFINSQ_2: 50;



           A26: ( addint "**" F2) = ( addint . (( addint "**" XFyX), 0 )) by A22, AFINSQ_2: 42

          .= (( addint "**" XFyX) + zz) by BINOP_2:def 20

          .= ( Sum XFyX) by AFINSQ_2: 50;



           A27: ( Sum (F1 ^ F2)) = (( Sum F1) + ( Sum F2)) by AFINSQ_2: 55

          .= (( addint "**" F1) + ( Sum F2)) by AFINSQ_2: 50

          .= ((( card Fyx) + (( - 1) * ( Sum XI))) + ( Sum XFyX)) by A24, A25, A26, AFINSQ_2: 50;



           A28: (urngFyX \/ Fyx) = urngFy by A3, A15, Th53;



           A29: (urngFyX /\ Fyx) = urngI by Th49;



           A30: ( dom FyX) = Xx by A3, RELAT_1: 62;

          then ( dom I) = Xx by Th48;

          then

           A31: ( card urngI) = ( Sum XI) by A2, A19, A20, A21;

          ( len <%( card Fyx)%>) = 1 & ( len XI1) = ( card Xx) by A19, AFINSQ_1: 33, VALUED_1:def 5;

          then

           A32: ( len F1) = (k + 1) by A16, AFINSQ_1: 17;



           A33: for n be Nat st n in ( dom XFS) holds (XFS . n) = ( addint . ((F1 . n),(F2 . n)))

          proof

            let n be Nat such that

             A34: n in ( dom XFS);



             A35: n < ( len XFS) by A34, AFINSQ_1: 86;

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

            per cases ;

              suppose

               A36: n = 0 ;



               A37: 0 in ( Segm k) by A14, NAT_1: 44;

              k = ( dom XFyX) by A3, A4, A15, A17, STIRL2_1: 55;

              then

               A38: (F2 . 0 ) = (XFyX . 0 ) & (XFyX . 0 ) = ((( - 1) |^ 0 ) * ( Card_Intersection (FyX,( 0 qua Nat + 1)))) by A18, AFINSQ_1:def 3, A37;

              (F1 . 0 ) = ( card Fyx) & (( - 1) |^ 0 ) = 1 by AFINSQ_1: 35, NEWTON: 4;

              then

               A39: ( addint . ((F1 . 0 ),(F2 . 0 ))) = (( card Fyx) + ( Card_Intersection (FyX,( 0 qua Nat + 1)))) by A38, BINOP_2:def 20;



               A40: (( - 1) |^ 0 ) = 1 by NEWTON: 4;

              (XFS . 0 ) = ((( - 1) |^ 0 ) * ( Card_Intersection (Fy,( 0 qua Nat + 1)))) by A6, A34, A36;

              hence thesis by A3, A15, A36, A39, A40, Th47;

            end;

              suppose

               A41: n > 0 ;

              then

              reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;



               A42: ( len <%( card Fyx)%>) = 1 by AFINSQ_1: 33;



               A43: ( card Xx) = k by A3, A4, A15, STIRL2_1: 55;



               A44: n < (k + 1) by A4, A5, A35;

              then

               A45: n <= k by NAT_1: 13;



               A46: n1 < (n1 + 1) by NAT_1: 13;

              then n1 < k by A45, XXREAL_0: 2;

              then n1 < ( len XI) by A19, A43;

              then n1 in ( dom XI) by AFINSQ_1: 86;

              then

               A47: (XI1 . n1) = (( - 1) * (XI . n1)) & (XI . n1) = ((( - 1) |^ n1) * ( Card_Intersection (I,(n1 + 1)))) by A20, VALUED_1: 6;

              ( 0 qua Nat + 1) <= n by A46, NAT_1: 13;

              then (F1 . n) = ((( - 1) * (( - 1) |^ n1)) * ( Card_Intersection (I,(n1 + 1)))) by A32, A44, A42, A47, AFINSQ_1: 19;

              then

               A48: (F1 . n) = ((( - 1) |^ (n1 + 1)) * ( Card_Intersection (I,(n1 + 1)))) by NEWTON: 6;



               A49: (XFS . n) = ((( - 1) |^ n) * ( Card_Intersection (Fy,(n + 1)))) by A6, A34;

              ( Card_Intersection (Fy,(n + 1))) = (( Card_Intersection (FyX,(n + 1))) + ( Card_Intersection (I,N))) by A3, A15, A30, A41, Th52;

              then

               A50: (XFS . n) = (((( - 1) |^ n) * ( Card_Intersection (FyX,(n + 1)))) + ((( - 1) |^ n) * ( Card_Intersection (I,N)))) by A49;

              per cases by A45, XXREAL_0: 1;

                suppose n < k;

                then

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

                ( card Xx) = k by A3, A4, A15, STIRL2_1: 55;

                then (XFyX . n) = ((( - 1) |^ n) * ( Card_Intersection (FyX,(n + 1)))) & (F2 . n) = (XFyX . n) by A17, A18, A51, AFINSQ_1:def 3;

                hence thesis by A50, A48, BINOP_2:def 20;

              end;

                suppose

                 A52: n = k;

                then n = ( card Xx) by A3, A4, A15, STIRL2_1: 55;

                then (n + 1) > ( card Xx) by NAT_1: 13;

                then

                 A53: ( Card_Intersection (FyX,(n + 1))) = 0 by A30, Th42;

                n = ( len XFyX) by A3, A4, A15, A17, A52, STIRL2_1: 55;

                then (F2 . n) = 0 by AFINSQ_1: 36;

                hence thesis by A50, A48, A53, BINOP_2:def 20;

              end;

            end;

          end;

          ( card urngFyX) = ( Sum XFyX) by A2, A30, A17, A18, A21;

          then

           A54: ( card urngFy) = ((( Sum XFyX) + ( card Fyx)) - ( Sum XI)) by A31, A28, A29, CARD_2: 45;



           A55: ( len <% 0 %>) = 1 by AFINSQ_1: 33;

          ( len XFyX) = ( card Xx) by A17;

          then

           A56: ( len F2) = (k + 1) by A55, A16, AFINSQ_1: 17;



           A57: ( len XFS) = (k + 1) by A4, A5;

          ( Sum XFS) = ( addint "**" XFS) by AFINSQ_2: 50

          .= ( addint "**" (F1 ^ F2)) by A32, A56, A33, A57, AFINSQ_2: 46

          .= ( Sum (F1 ^ F2)) by AFINSQ_2: 50;

          hence thesis by A27, A54;

        end;

      end;



       A58: P[ 0 ]

      proof

        let Fy be finite-yielding Function, X such that

         A59: ( dom Fy) = X and

         A60: ( card X) = 0 ;

        ( dom Fy) = {} by A59, A60;

        then

         A61: ( rng Fy) = {} by RELAT_1: 42;

        let XFS be XFinSequence of INT such that

         A62: ( dom XFS) = ( card X) and for n st n in ( dom XFS) holds (XFS . n) = ((( - 1) |^ n) * ( Card_Intersection (Fy,(n + 1))));

        ( len XFS) = 0 by A60, A62;



        then ( addint "**" XFS) = ( the_unity_wrt addint ) by AFINSQ_2:def 8

        .= 0 by BINOP_2: 4;

        hence thesis by A61, AFINSQ_2: 50, ZFMISC_1: 2;

      end;

      for k holds P[k] from NAT_1:sch 2( A58, A1);

      hence thesis;

    end;

    theorem :: CARD_FIN:57



     Th56: for Fy, X, n, k st ( dom Fy) = X holds (ex x, y st x <> y & for f st f in ( Choose (X,k,x,y)) holds ( card ( Intersection (Fy,f,x))) = n) implies ( Card_Intersection (Fy,k)) = (n * (( card X) choose k))

    proof

      let Fy, X, n, k such that

       A1: X = ( dom Fy);

      assume ex x, y st x <> y & for f st f in ( Choose (X,k,x,y)) holds ( card ( Intersection (Fy,f,x))) = n;

      then

      consider x, y such that

       A2: x <> y and

       A3: for f st f in ( Choose (X,k,x,y)) holds ( card ( Intersection (Fy,f,x))) = n;

      set Ch = ( Choose (X,k,x,y));

      consider P be Function of ( card Ch), Ch such that

       A4: P is one-to-one by Lm2;

      consider XFS be XFinSequence of NAT such that

       A5: ( dom XFS) = ( dom P) and

       A6: for z, f st z in ( dom XFS) & f = (P . z) holds (XFS . z) = ( card ( Intersection (Fy,f,x))) and

       A7: ( Card_Intersection (Fy,k)) = ( Sum XFS) by A1, A2, A4, Def3;

      for z be object st z in ( dom XFS) holds (XFS . z) = n

      proof

        let z be object such that

         A8: z in ( dom XFS);



         A9: (P . z) in ( rng P) by A5, A8, FUNCT_1:def 3;

        then

        consider f be Function of X, {x, y} such that

         A10: f = (P . z) and ( card (f " {x})) = k by Def1;

        (XFS . z) = ( card ( Intersection (Fy,f,x))) by A6, A8, A10;

        hence thesis by A3, A9, A10;

      end;

      then

       A11: XFS = (( dom XFS) --> n) by FUNCOP_1: 11;

      then

       A12: ( rng XFS) c= {n} by FUNCOP_1: 13;

      Ch = {} implies ( card Ch) = {} ;

      then

       A13: ( dom P) = ( card Ch) by FUNCT_2:def 1;

      n in {n} by TARSKI:def 1;

      then {n} c= { 0 , n} & (XFS " {n}) = ( dom P) by A5, A11, FUNCOP_1: 14, ZFMISC_1: 7;

      then ( Sum XFS) = (n * ( card ( card Ch))) by A12, A13, AFINSQ_2: 68, XBOOLE_1: 1;

      hence thesis by A2, A7, Th15;

    end;

    theorem :: CARD_FIN:58



     Th57: for Fy, X st ( dom Fy) = X holds for XF be XFinSequence of NAT st ( dom XF) = ( card X) & for n st n in ( dom XF) holds ex x, y st x <> y & for f st f in ( Choose (X,(n + 1),x,y)) holds ( card ( Intersection (Fy,f,x))) = (XF . n) holds ex F be XFinSequence of INT st ( dom F) = ( card X) & ( card ( union ( rng Fy))) = ( Sum F) & for n st n in ( dom F) holds (F . n) = (((( - 1) |^ n) * (XF . n)) * (( card X) choose (n + 1)))

    proof

      let Fy, X such that

       A1: ( dom Fy) = X;

      let XF be XFinSequence of NAT such that

       A2: ( dom XF) = ( card X) & for n st n in ( dom XF) holds ex x, y st x <> y & for f st f in ( Choose (X,(n + 1),x,y)) holds ( card ( Intersection (Fy,f,x))) = (XF . n);

      defpred f[ object, object] means for n st n = $1 holds $2 = (((( - 1) |^ n) * (XF . n)) * (( card X) choose (n + 1)));



       A3: for x be object st x in ( card X) holds ex y be object st y in INT & f[x, y]

      proof



         A4: ( card X) is Subset of NAT by STIRL2_1: 8;

        let x be object;

        assume x in ( card X);

        then

        reconsider x9 = x as Element of NAT by A4;

        reconsider xx = ((( - 1) |^ x9) * (XF . x9)) as Integer;

        reconsider ch = (( card X) choose (x9 + 1)) as Integer;

        take (xx * ch);

        thus thesis by INT_1:def 2;

      end;

      consider F be Function of ( card X), INT such that

       A5: for x be object st x in ( card X) holds f[x, (F . x)] from FUNCT_2:sch 1( A3);



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

      then

      reconsider F as XFinSequence by AFINSQ_1: 5;

      reconsider F as XFinSequence of INT ;

      take F;

      for n st n in ( dom F) holds (F . n) = ((( - 1) |^ n) * ( Card_Intersection (Fy,(n + 1))))

      proof

        let n such that

         A7: n in ( dom F);

        ex x, y st x <> y & for f st f in ( Choose (X,(n + 1),x,y)) holds ( card ( Intersection (Fy,f,x))) = (XF . n) by A2, A6, A7;

        then

         A8: ( Card_Intersection (Fy,(n + 1))) = ((XF . n) * (( card X) choose (n + 1))) by A1, Th56;

        (F . n) = (((( - 1) |^ n) * (XF . n)) * (( card X) choose (n + 1))) by A5, A6, A7;

        hence thesis by A8;

      end;

      hence thesis by A1, A5, A6, Th55;

    end;



     Lm3: for X,Y be finite set st X is non empty & Y is non empty holds ex F be XFinSequence of INT st ( dom F) = ( card Y) & ((( card Y) |^ ( card X)) - ( Sum F)) = ( card { f where f be Function of X, Y : f is onto }) & for n st n in ( dom F) holds (F . n) = (((( - 1) |^ n) * (( card Y) choose (n + 1))) * (((( card Y) - n) - 1) |^ ( card X)))

    proof

      let X,Y be finite set such that

       A1: X is non empty and

       A2: Y is non empty;

      defpred xf[ object, object] means for n st n = $1 holds $2 = (((( card Y) - n) - 1) |^ ( card X));



       A3: for x be object st x in ( Segm ( card Y)) holds ex y be object st y in NAT & xf[x, y]

      proof

        let x be object such that

         A4: x in ( Segm ( card Y));

        reconsider n = x as Element of NAT by A4;

        n < ( card Y) by A4, NAT_1: 44;

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

        then

        reconsider k = (( card Y) - (n + 1)) as Element of NAT by NAT_1: 21;

         xf[n, (k |^ ( card X))];

        hence thesis;

      end;

      consider XF be Function of ( Segm ( card Y)), NAT such that

       A5: for x be object st x in ( Segm ( card Y)) holds xf[x, (XF . x)] from FUNCT_2:sch 1( A3);

      set Onto = { f where f be Function of X, Y : f is onto };

      deffunc fy( object) = { f where f be Function of X, Y : not $1 in ( rng f) };



       A6: for x be object st x in Y holds fy(x) in ( bool ( Funcs (X,Y)))

      proof

        let x be object such that

         A7: x in Y;

         fy(x) c= ( Funcs (X,Y))

        proof

          let y be object;

          assume y in fy(x);

          then ex f be Function of X, Y st y = f & not x in ( rng f);

          hence thesis by A7, FUNCT_2: 8;

        end;

        hence thesis;

      end;

      consider Fy9 be Function of Y, ( bool ( Funcs (X,Y))) such that

       A8: for x be object st x in Y holds (Fy9 . x) = fy(x) from FUNCT_2:sch 2( A6);

      for y be object st y in ( dom Fy9) holds (Fy9 . y) is finite

      proof

        let y be object;

        assume y in ( dom Fy9);

        then (Fy9 . y) in ( rng Fy9) by FUNCT_1:def 3;

        hence thesis;

      end;

      then

      reconsider Fy = Fy9 as finite-yielding Function by FINSET_1:def 4;

      ( union ( rng Fy9)) c= ( union ( bool ( Funcs (X,Y)))) by ZFMISC_1: 77;

      then

       A9: ( union ( rng Fy)) c= ( Funcs (X,Y)) by ZFMISC_1: 81;

      reconsider u = ( union ( rng Fy)) as finite set;



       A10: ( dom XF) = ( card Y) by FUNCT_2:def 1;

      then

      reconsider XF as XFinSequence by AFINSQ_1: 5;

      reconsider XF as XFinSequence of NAT ;



       A11: for n st n in ( dom XF) holds ex x, y st x <> y & for f st f in ( Choose (Y,(n + 1),x,y)) holds ( card ( Intersection (Fy,f,x))) = (XF . n)

      proof

        let n such that

         A12: n in ( dom XF);

        take 0 , 1;

        thus 0 <> 1;

        let f9 be Function;

        assume f9 in ( Choose (Y,(n + 1), 0 ,1));

        then

        consider f be Function of Y, { 0 , 1} such that

         A13: f = f9 and

         A14: ( card (f " { 0 })) = (n + 1) by Def1;



         A15: ( Intersection (Fy,f, 0 )) c= ( Funcs (X,(Y \ (f " { 0 }))))

        proof

          let z be object such that

           A16: z in ( Intersection (Fy,f, 0 ));

           0 in ( rng f) by A14, CARD_1: 27, FUNCT_1: 72;

          then

          consider x1 such that

           A17: x1 in ( dom f) and (f . x1) = 0 and

           A18: z in (Fy . x1) by A16, Th21;

          z in fy(x1) by A8, A17, A18;

          then

          consider g be Function of X, Y such that

           A19: z = g and not x1 in ( rng g);



           A20: ( rng g) c= (Y \ (f " { 0 }))

          proof

            let gy be object such that

             A21: gy in ( rng g);

            assume not gy in (Y \ (f " { 0 }));

            then

             A22: gy in (f " { 0 }) by A21, XBOOLE_0:def 5;

            then (f . gy) in { 0 } by FUNCT_1:def 7;

            then

             A23: (f . gy) = 0 by TARSKI:def 1;

            gy in ( dom f) by A22, FUNCT_1:def 7;

            then g in (Fy . gy) by A16, A19, A23, Def2;

            then g in fy(gy) by A8, A21;

            then ex h be Function of X, Y st g = h & not gy in ( rng h);

            hence contradiction by A21;

          end;

          ( dom g) = X by A17, FUNCT_2:def 1;

          hence thesis by A19, A20, FUNCT_2:def 2;

        end;

        reconsider I = ( Intersection (Fy,f, 0 )) as finite set;



         A24: ( card (Y \ (f " { 0 }))) = (( card Y) - (n + 1)) by A14, CARD_2: 44;

        ( Funcs (X,(Y \ (f " { 0 })))) c= ( Intersection (Fy,f, 0 ))

        proof

          let g9 be object;

          assume g9 in ( Funcs (X,(Y \ (f " { 0 }))));

          then

          consider g be Function such that

           A25: g9 = g and

           A26: ( dom g) = X and

           A27: ( rng g) c= (Y \ (f " { 0 })) by FUNCT_2:def 2;

          reconsider gg = g as Function of X, Y by A26, A27, FUNCT_2: 2, XBOOLE_1: 1;

          consider y be object such that

           A28: y in (f " { 0 }) by A14, CARD_1: 27, XBOOLE_0:def 1;

           not y in ( rng g) by A27, A28, XBOOLE_0:def 5;

          then

           A29: gg in fy(y);

          ( dom Fy) = Y by FUNCT_2:def 1;

          then

           A30: (Fy9 . y) in ( rng Fy9) by A28, FUNCT_1:def 3;



           A31: for z st z in ( dom f) & (f . z) = 0 holds g in (Fy . z)

          proof

            let z such that

             A32: z in ( dom f) and

             A33: (f . z) = 0 ;

            (f . z) in { 0 } by A33, TARSKI:def 1;

            then z in (f " { 0 }) by A32, FUNCT_1:def 7;

            then

             A34: not z in ( rng gg) by A27, XBOOLE_0:def 5;

            (Fy . z) = fy(z) by A8, A32;

            hence thesis by A34;

          end;

           fy(y) = (Fy9 . y) by A8, A28;

          then g in ( union ( rng Fy)) by A30, A29, TARSKI:def 4;

          hence thesis by A25, A31, Def2;

        end;

        then

         A35: ( Funcs (X,(Y \ (f " { 0 })))) = ( Intersection (Fy,f, 0 )) by A15;

        now

          per cases ;

            suppose (Y \ (f " { 0 })) = {} ;

            then ( card I) = 0 & (((( card Y) - n) - 1) |^ ( card X)) = 0 by A1, A15, A24, NAT_1: 14, NEWTON: 11;

            hence thesis by A5, A10, A12, A13;

          end;

            suppose

             A36: (Y \ (f " { 0 })) <> {} ;

            (XF . n) = (((( card Y) - n) - 1) |^ ( card X)) by A5, A10, A12;

            hence thesis by A13, A35, A24, A36, Th3;

          end;

        end;

        hence thesis;

      end;

      ( dom XF) = ( card Y) & ( dom Fy) = Y by FUNCT_2:def 1;

      then

      consider F be XFinSequence of INT such that

       A37: ( dom F) = ( card Y) and

       A38: ( card ( union ( rng Fy))) = ( Sum F) and

       A39: for n st n in ( dom F) holds (F . n) = (((( - 1) |^ n) * (XF . n)) * (( card Y) choose (n + 1))) by A11, Th57;

      take F;

      thus ( dom F) = ( card Y) by A37;



       A40: ( card (( Funcs (X,Y)) \ u)) = (( card ( Funcs (X,Y))) - ( card u)) by A9, CARD_2: 44;



       A41: Onto c= (( Funcs (X,Y)) \ ( union ( rng Fy)))

      proof

        let x be object;

        assume x in Onto;

        then

        consider f be Function of X, Y such that

         A42: x = f and

         A43: f is onto;

        assume

         A44: not x in (( Funcs (X,Y)) \ ( union ( rng Fy)));

        f in ( Funcs (X,Y)) by A2, FUNCT_2: 8;

        then f in ( union ( rng Fy)) by A42, A44, XBOOLE_0:def 5;

        then

        consider Fyy be set such that

         A45: f in Fyy and

         A46: Fyy in ( rng Fy) by TARSKI:def 4;

        consider y be object such that

         A47: y in ( dom Fy) and

         A48: (Fy . y) = Fyy by A46, FUNCT_1:def 3;

        y in Y by A47, FUNCT_2:def 1;

        then f in fy(y) by A8, A45, A48;

        then

         A49: ex g be Function of X, Y st f = g & not y in ( rng g);

        y in Y by A47, FUNCT_2:def 1;

        hence contradiction by A43, A49, FUNCT_2:def 3;

      end;



       A50: (( Funcs (X,Y)) \ ( union ( rng Fy))) c= Onto

      proof

        let x be object such that

         A51: x in (( Funcs (X,Y)) \ ( union ( rng Fy)));

        consider f such that

         A52: x = f and

         A53: ( dom f) = X & ( rng f) c= Y by A51, FUNCT_2:def 2;

        reconsider f as Function of X, Y by A53, FUNCT_2: 2;

        assume not x in Onto;

        then not f is onto by A52;

        then ( rng f) <> Y by FUNCT_2:def 3;

        then not Y c= ( rng f);

        then

        consider y be object such that

         A54: y in Y and

         A55: not y in ( rng f);

        y in ( dom Fy9) by A54, FUNCT_2:def 1;

        then (Fy9 . y) in ( rng Fy9) by FUNCT_1:def 3;

        then

         A56: fy(y) in ( rng Fy9) by A8, A54;

        f in fy(y) by A55;

        then f in ( union ( rng Fy)) by A56, TARSKI:def 4;

        hence thesis by A51, A52, XBOOLE_0:def 5;

      end;

      ( card ( Funcs (X,Y))) = (( card Y) |^ ( card X)) by A2, Th3;

      hence ( card Onto) = ((( card Y) |^ ( card X)) - ( Sum F)) by A38, A50, A41, A40, XBOOLE_0:def 10;

      let n such that

       A57: n in ( dom F);



       A58: (F . n) = (((( - 1) |^ n) * (XF . n)) * (( card Y) choose (n + 1))) by A39, A57;

      (XF . n) = (((( card Y) - n) - 1) |^ ( card X)) by A5, A37, A57;

      hence thesis by A58;

    end;

    theorem :: CARD_FIN:59



     Th58: for X,Y be finite set st X is non empty & Y is non empty holds ex F be XFinSequence of INT st ( dom F) = (( card Y) + 1) & ( Sum F) = ( card { f where f be Function of X, Y : f is onto }) & for n st n in ( dom F) holds (F . n) = (((( - 1) |^ n) * (( card Y) choose n)) * ((( card Y) - n) |^ ( card X)))

    proof

      let X,Y be finite set such that

       A1: X is non empty & Y is non empty;

      reconsider c = (( card Y) |^ ( card X)) as Element of INT by INT_1:def 2;



       A2: ( len <%c%>) = 1 by AFINSQ_1: 33;

      set Onto = { f where f be Function of X, Y : f is onto };

      consider F be XFinSequence of INT such that

       A3: ( dom F) = ( card Y) and

       A4: ((( card Y) |^ ( card X)) - ( Sum F)) = ( card Onto) and

       A5: for n st n in ( dom F) holds (F . n) = (((( - 1) |^ n) * (( card Y) choose (n + 1))) * (((( card Y) - n) - 1) |^ ( card X))) by A1, Lm3;

      set F1 = (( - 1) (#) F);

      reconsider F1 as XFinSequence of INT ;



       A6: ( dom F1) = ( dom F) & ( dom F) = ( card Y) by A3, VALUED_1:def 5;

      reconsider GF1 = ( <%c%> ^ F1) as XFinSequence of INT ;

      take GF1;

      ( len F1) = ( card Y) by A3, VALUED_1:def 5;

      hence

       A7: ( dom GF1) = (( card Y) + 1) by A2, AFINSQ_1:def 3;

      (( - 1) * ( Sum F)) = ( Sum F1) by AFINSQ_2: 64;



      then (c - ( Sum F)) = (c + ( Sum F1))

      .= ( addint . (c,( Sum F1))) by BINOP_2:def 20

      .= ( addint . (( addint "**" <%c%>),( Sum F1))) by AFINSQ_2: 37

      .= ( addint . (( addint "**" <%c%>),( addint "**" F1))) by AFINSQ_2: 50

      .= ( addint "**" GF1) by AFINSQ_2: 42

      .= ( Sum GF1) by AFINSQ_2: 50;

      hence ( Sum GF1) = ( card Onto) by A4;

      let n such that

       A8: n in ( dom GF1);

      now

        per cases ;

          suppose

           A9: n = 0 ;

          then (( - 1) |^ n) = 1 & (( card Y) choose n) = 1 by NEWTON: 4, NEWTON: 19;

          hence thesis by A9, AFINSQ_1: 35;

        end;

          suppose n > 0 ;

          then

          reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

          n < ( len GF1) by A8, AFINSQ_1: 86;

          then n < (( card Y) + 1) by A7;

          then (n1 + 1) <= ( card Y) by NAT_1: 13;

          then n1 < ( card Y) by NAT_1: 13;

          then n1 < ( len F1) by A6;

          then

           A10: n1 in ( dom F1) by AFINSQ_1: 86;

          then

           A11: (F . n1) = (((( - 1) |^ n1) * (( card Y) choose (n1 + 1))) * (((( card Y) - n1) - 1) |^ ( card X))) by A5, A6;

          ( len <%c%>) = 1 by AFINSQ_1: 33;

          then

           A12: (GF1 . (n1 + 1)) = (F1 . n1) by A10, AFINSQ_1:def 3;

          then

           A13: (( - 1) * (( - 1) |^ n1)) = (( - 1) |^ n) by NEWTON: 6;

          (GF1 . (n1 + 1)) = (( - 1) * (F . n1)) by A12, VALUED_1: 6;

          hence thesis by A11, A13;

        end;

      end;

      hence thesis;

    end;

    theorem :: CARD_FIN:60

    for n, k st k <= n holds ex F be XFinSequence of INT st (n block k) = ((1 / (k ! )) * ( Sum F)) & ( dom F) = (k + 1) & for m st m in ( dom F) holds (F . m) = (((( - 1) |^ m) * (k choose m)) * ((k - m) |^ n))

    proof

      let n, k such that

       A1: k <= n;

      now

        per cases ;

          suppose

           A2: n = 0 & k = 0 ;

          reconsider I = 1 as Element of INT by INT_1:def 2;

          set F = <%I%>;

          take F;

          ( addint "**" <%I%>) = 1 by AFINSQ_2: 37;

          then ( Sum F) = 1 by AFINSQ_2: 50;

          hence (n block k) = ((1 / (k ! )) * ( Sum F)) by A2, NEWTON: 12, STIRL2_1: 26;

          thus ( dom F) = (k + 1) by A2, AFINSQ_1: 33;

          let m;

          assume m in ( dom F);

          then

           A3: m in { 0 } by AFINSQ_1: 33, CARD_1: 49;

          then m = 0 by TARSKI:def 1;

          then

           A4: (( - 1) |^ m) = 1 by NEWTON: 4;



           A5: ((k - m) |^ n) = 1 by A2, NEWTON: 4;



           A6: ( 0 choose 0 ) = 1 by NEWTON: 19;

          m = 0 by A3, TARSKI:def 1;

          hence (F . m) = (((( - 1) |^ m) * (k choose m)) * ((k - m) |^ n)) by A2, A4, A5, A6;

        end;

          suppose

           A7: n <> 0 & k = 0 ;

          set F = ((k + 1) --> 0 );

          reconsider Fi = F as XFinSequence of INT ;

          reconsider Fn = F as XFinSequence of NAT ;

          take Fi;

          ( rng F) c= { 0 } & { 0 } c= { 0 , 0 } by ENUMSET1: 29, FUNCOP_1: 13;

          then ( Sum Fn) = ( 0 * ( card (Fn " { 0 }))) by AFINSQ_2: 68, XBOOLE_1: 1;

          hence (n block k) = ((1 / (k ! )) * ( Sum Fi)) & ( dom Fi) = (k + 1) by A7, STIRL2_1: 31;

          let m such that m in ( dom Fi);

          now

            per cases ;

              suppose m = 0 ;

              then ((k - m) |^ n) = 0 by A7, NAT_1: 14, NEWTON: 11;

              hence ((k choose m) * ((k - m) |^ n)) = 0 ;

            end;

              suppose m > 0 ;

              then (k choose m) = 0 by A7, NEWTON:def 3;

              hence ((k choose m) * ((k - m) |^ n)) = 0 ;

            end;

          end;

          then

           A9: ((( - 1) |^ m) * ((k choose m) * ((k - m) |^ n))) = 0 ;

          thus (Fi . m) = (((( - 1) |^ m) * (k choose m)) * ((k - m) |^ n)) by A9;

        end;

          suppose

           A10: n <> 0 & k <> 0 ;

          set Perm = { p where p be Function of k, k : p is Permutation of k };

          ( card Perm) = (( card k) ! ) by Th7;

          then

          reconsider Perm as finite set;

          reconsider Bloc = { f where f be Function of ( Segm n), ( Segm k) : f is onto "increasing } as finite set by STIRL2_1: 24;

          set Onto = { f where f be Function of n, k : f is onto };

          defpred P[ object, object] means for p be Function of k, k, f be Function of n, k st $1 = [p, f] holds $2 = (p * f);

          reconsider N = n, K = k as non empty Subset of NAT by A10, STIRL2_1: 8;



           A11: ( card [:Perm, Bloc:]) = (( card Perm) * ( card Bloc)) by CARD_2: 46;



           A12: for x be object st x in [:Perm, Bloc:] holds ex y be object st y in Onto & P[x, y]

          proof

            let x be object;

            assume x in [:Perm, Bloc:];

            then

            consider p9,f9 be object such that

             A13: p9 in Perm and

             A14: f9 in Bloc and

             A15: x = [p9, f9] by ZFMISC_1:def 2;

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

             A16: f = f9 and

             A17: f is onto "increasing by A14;



             A18: ( rng f) = ( Segm k) by A17, FUNCT_2:def 3;

            consider p be Function of ( Segm k), ( Segm k) such that

             A19: p = p9 and

             A20: p is Permutation of ( Segm k) by A13;

            reconsider pf = (p * f) as Function of ( Segm n), ( Segm k);

            take pf;



             A21: ( dom p) = ( Segm k) by A10, FUNCT_2:def 1;

            ( rng p) = k by A20, FUNCT_2:def 3;

            then ( rng (p * f)) = k by A18, A21, RELAT_1: 28;

            then pf is onto by FUNCT_2:def 3;

            hence pf in Onto;

            let p1 be Function of k, k, f1 be Function of n, k such that

             A22: x = [p1, f1];

            p1 = p by A15, A19, A22, XTUPLE_0: 1;

            hence thesis by A15, A16, A22, XTUPLE_0: 1;

          end;

          consider FP be Function of [:Perm, Bloc:], Onto such that

           A23: for x be object st x in [:Perm, Bloc:] holds P[x, (FP . x)] from FUNCT_2:sch 1( A12);



           A24: FP is one-to-one

          proof

            let x1,x2 be object such that

             A25: x1 in ( dom FP) and

             A26: x2 in ( dom FP) and

             A27: (FP . x1) = (FP . x2);

            consider p19,f19 be object such that

             A28: p19 in Perm and

             A29: f19 in Bloc and

             A30: x1 = [p19, f19] by A25, ZFMISC_1:def 2;

            consider p1 be Function of k, k such that

             A31: p19 = p1 and

             A32: p1 is Permutation of k by A28;

            consider p29,f29 be object such that

             A33: p29 in Perm and

             A34: f29 in Bloc and

             A35: x2 = [p29, f29] by A26, ZFMISC_1:def 2;

            (FP . x1) in ( rng FP) by A25, FUNCT_1:def 3;

            then (FP . x1) in Onto;

            then

            consider fp be Function of N, K such that

             A36: (FP . x1) = fp and

             A37: fp is onto;



             A38: ( rng fp) = K by A37, FUNCT_2:def 3;

            consider p2 be Function of k, k such that

             A39: p29 = p2 and

             A40: p2 is Permutation of k by A33;

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

             A41: f29 = f2 and

             A42: f2 is onto "increasing by A34;

            ( rng fp) = K by A37, FUNCT_2:def 3;

            then

            reconsider p199 = p1, p299 = p2 as Permutation of ( rng fp) by A32, A40;

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

             A43: f19 = f1 and

             A44: f1 is onto "increasing by A29;

            reconsider f199 = f1, f299 = f2 as Function of N, K;



             A45: ( rng f2) = K by A42, FUNCT_2:def 3;

            for l,m be Nat st l in ( rng f1) & m in ( rng f1) & l < m holds ( min* (f1 " {l})) < ( min* (f1 " {m})) by A44, STIRL2_1:def 1;

            then

             A46: f199 is 'increasing by STIRL2_1:def 3;

            for l,m be Nat st l in ( rng f2) & m in ( rng f2) & l < m holds ( min* (f2 " {l})) < ( min* (f2 " {m})) by A42, STIRL2_1:def 1;

            then

             A47: f299 is 'increasing by STIRL2_1:def 3;



             A48: fp = (p199 * f199) by A23, A25, A30, A31, A43, A36;



             A49: ( rng f1) = K by A44, FUNCT_2:def 3;



             A50: fp = (p299 * f299) by A23, A26, A27, A35, A39, A41, A36;

            then p199 = p299 by A46, A47, A49, A45, A48, A38, STIRL2_1: 65;

            hence thesis by A30, A31, A43, A35, A39, A41, A46, A47, A49, A45, A48, A50, A38, STIRL2_1: 65;

          end;

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

           A51: h is onto "increasing by A1, A10, STIRL2_1: 23;

          Onto c= ( rng FP)

          proof

            let x be object;

            assume x in Onto;

            then

            consider f be Function of n, k such that

             A52: f = x and

             A53: f is onto;

            ( rng f) = K by A53, FUNCT_2:def 3;

            then

            consider I be Function of N, K, P be Permutation of K such that

             A54: f = (P * I) and

             A55: K = ( rng I) and

             A56: I is 'increasing by STIRL2_1: 63;

            set p = P;

            reconsider i = I as Function of ( Segm n), ( Segm k);

            for l,m be Nat st l in ( rng I) & m in ( rng I) & l < m holds ( min* (I " {l})) < ( min* (I " {m})) by A56, STIRL2_1:def 3;

            then

             A57: i is "increasing by STIRL2_1:def 1;

            i is onto by A55, FUNCT_2:def 3;

            then p in Perm & i in Bloc by A57;

            then

             A58: [p, i] in [:Perm, Bloc:] by ZFMISC_1:def 2;

            h in Onto by A51;

            then

             A59: [p, i] in ( dom FP) by A58, FUNCT_2:def 1;

            (FP . [p, i]) = f by A23, A54, A58;

            hence thesis by A52, A59, FUNCT_1:def 3;

          end;

          then

           A60: ( rng FP) = Onto;

          h in Onto by A51;

          then ( dom FP) = [:Perm, Bloc:] by FUNCT_2:def 1;

          then (Onto, [:Perm, Bloc:]) are_equipotent by A24, A60, WELLORD2:def 4;

          then

           A61: ( card Onto) = (( card Perm) * ( card Bloc)) by A11, CARD_1: 5;



           A62: (((k ! ) * ( card Bloc)) / (k ! )) = (( card Bloc) * ((k ! ) / (k ! ))) & ((k ! ) / (k ! )) = 1 by XCMPLX_1: 60, XCMPLX_1: 74;

          consider F be XFinSequence of INT such that

           A63: ( dom F) = (( card k) + 1) and

           A64: ( Sum F) = ( card { f where f be Function of n, k : f is onto }) and

           A65: for m st m in ( dom F) holds (F . m) = (((( - 1) |^ m) * (( card k) choose m)) * ((( card k) - m) |^ ( card n))) by A10, Th58;

          take F;

          ( card Perm) = (( card k) ! ) by Th7;

          then ( Sum F) = ((k ! ) * ( card Bloc)) by A64, A61;

          then (n block k) = ((( Sum F) * 1) / (k ! )) by A62, STIRL2_1:def 2;

          hence (n block k) = ((1 / (k ! )) * ( Sum F)) by XCMPLX_1: 74;

          thus ( dom F) = (k + 1) by A63;

          let m;

          assume m in ( dom F);

          hence (F . m) = (((( - 1) |^ m) * (k choose m)) * ((k - m) |^ n)) by A65;

        end;

          suppose n = 0 & k <> 0 ;

          hence thesis by A1;

        end;

      end;

      hence thesis;

    end;

    theorem :: CARD_FIN:61



     Th60: for X1,Y1,X be finite set st (Y1 is empty implies X1 is empty) & X c= X1 holds for F be Function of X1, Y1 st F is one-to-one & ( card X1) = ( card Y1) holds ((( card X1) -' ( card X)) ! ) = ( card { f where f be Function of X1, Y1 : f is one-to-one & ( rng (f | (X1 \ X))) c= (F .: (X1 \ X)) & for x st x in X holds (f . x) = (F . x) })

    proof

      let X1,Y1,X be finite set such that

       A1: Y1 is empty implies X1 is empty and

       A2: X c= X1;

      set XX = (X1 \ X);

      let F be Function of X1, Y1 such that

       A3: F is one-to-one and

       A4: ( card X1) = ( card Y1);

      deffunc F( set) = (F . $1);

      defpred P[ Function, set, set] means $1 is one-to-one & ( rng ($1 | XX)) = (F .: XX);

      reconsider FX = (F .: XX) as finite set;

      set F1 = { f where f be Function of XX, (F .: XX) : f is one-to-one };



       A5: ( card XX) = (( card X1) - ( card X)) by A2, CARD_2: 44;



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

      proof

        let f be Function of X1, Y1 such that

         A7: for x st x in (X1 \ XX) holds F(x) = (f . x);

        thus P[f, X1, Y1] implies P[(f | XX), XX, (F .: XX)] by FUNCT_1: 52;

        thus P[(f | XX), XX, (F .: XX)] implies P[f, X1, Y1]

        proof

          F is onto by A3, A4, FINSEQ_4: 63;

          then

           A8: ( rng F) = Y1 by FUNCT_2:def 3;



           A9: ( rng (f | XX)) = (f .: XX) & (F .: ((X1 \ XX) \/ XX)) = ((F .: (X1 \ XX)) \/ (F .: XX)) by RELAT_1: 115, RELAT_1: 120;



           A10: ( dom (F | (X1 \ XX))) = (( dom F) /\ (X1 \ XX)) & ( dom F) = X1 by A1, FUNCT_2:def 1, RELAT_1: 61;



           A11: ( dom (f | (X1 \ XX))) = (( dom f) /\ (X1 \ XX)) & ( dom f) = X1 by A1, FUNCT_2:def 1, RELAT_1: 61;

          now



             A12: (X1 \ XX) = (X /\ X1) & (X /\ X1) = X by A2, XBOOLE_1: 28, XBOOLE_1: 48;

            let x be object such that

             A13: x in ( dom (F | (X1 \ XX)));

            (f . x) = ((f | (X1 \ XX)) . x) by A11, A10, A13, FUNCT_1: 47;

            hence (F . x) = ((f | (X1 \ XX)) . x) by A7, A10, A13, A12;

          end;

          then (f | (X1 \ XX)) = (F | (X1 \ XX)) by A11, A10, FUNCT_1: 46;

          then

           A14: ( rng (f | (X1 \ XX))) = (F .: (X1 \ XX)) by RELAT_1: 115;



           A15: ((X1 \ XX) \/ XX) = X1 & ( rng (f | (X1 \ XX))) = (f .: (X1 \ XX)) by RELAT_1: 115, XBOOLE_1: 45;



           A16: X1 = ( dom F) & X1 = ( dom f) by A1, FUNCT_2:def 1;



           A17: (F .: ( dom F)) = ( rng F) by RELAT_1: 113;

          assume

           A18: P[(f | XX), XX, (F .: XX)];

          then ( rng (f | XX)) = (F .: XX);

          then (F .: X1) = (f .: X1) by A14, A15, A9, RELAT_1: 120;

          then ( rng F) = ( rng f) by A16, A17, RELAT_1: 113;

          then f is onto by A8, FUNCT_2:def 3;

          hence thesis by A4, A18, FINSEQ_4: 63;

        end;

      end;

      set F2 = { f where f be Function of X1, Y1 : f is one-to-one & ( rng (f | XX)) c= (F .: XX) & for x st x in X holds (f . x) = (F . x) };

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



       A19: (X1 \ XX) = (X /\ X1) & (X /\ X1) = X by A2, XBOOLE_1: 28, XBOOLE_1: 48;



       A20: S2 c= F2

      proof

        let x be object;

        assume x in S2;

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

        hence thesis by A19;

      end;

      ( dom F) = X1 by A1, FUNCT_2:def 1;

      then (XX,(F .: XX)) are_equipotent by A3, CARD_1: 33;

      then

       A21: ( card XX) = ( card (F .: XX)) by CARD_1: 5;

      then ( card F1) = ((( card XX) ! ) / ((( card FX) -' ( card XX)) ! )) & (( card FX) -' ( card XX)) = 0 by Th6, XREAL_1: 232;

      then

       A22: ( card F1) = ((( card X1) -' ( card X)) ! ) by A5, NEWTON: 12, XREAL_0:def 2;

      set S1 = { f where f be Function of XX, (F .: XX) : P[f, XX, (F .: XX)] };



       A23: for x st x in (X1 \ XX) holds F(x) in Y1

      proof



         A24: X1 = ( dom F) by A1, FUNCT_2:def 1;

        let x;

        assume x in (X1 \ XX);

        then (F . x) in ( rng F) by A24, FUNCT_1:def 3;

        hence thesis;

      end;



       A25: F1 c= S1

      proof

        let x be object;

        assume x in F1;

        then

        consider f be Function of XX, FX such that

         A26: x = f and

         A27: f is one-to-one;



         A28: (f | XX) = f;

        f is onto by A21, A27, FINSEQ_4: 63;

        then ( rng f) = FX by FUNCT_2:def 3;

        hence thesis by A26, A27, A28;

      end;

      S1 c= F1

      proof

        let x be object;

        assume x in S1;

        then ex f be Function of XX, FX st f = x & P[f, XX, (F .: XX)];

        hence thesis;

      end;

      then

       A29: F1 = S1 by A25;



       A30: F2 c= S2

      proof

        let x be object;

        assume x in F2;

        then

        consider f be Function of X1, Y1 such that

         A31: x = f and

         A32: f is one-to-one and

         A33: ( rng (f | XX)) c= (F .: XX) and

         A34: for x st x in X holds (f . x) = (F . x);

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

        then (XX,(f .: XX)) are_equipotent by A32, CARD_1: 33;

        then ( card XX) = ( card (f .: XX)) by CARD_1: 5;

        then ( card FX) = ( card ( rng (f | XX))) by A21, RELAT_1: 115;

        then ( rng (f | XX)) = FX by A33, CARD_2: 102;

        hence thesis by A19, A31, A32, A34;

      end;



       A35: XX c= X1 & (F .: XX) c= Y1;

      then XX c= ( dom F) by A1, FUNCT_2:def 1;

      then

       A36: (F .: XX) is empty implies XX is empty by RELAT_1: 119;

      ( card S1) = ( card S2) from STIRL2_1:sch 3( A23, A35, A36, A6);

      hence thesis by A20, A30, A22, A29, XBOOLE_0:def 10;

    end;



     Lm4: for X, Y holds for F be Function of X, Y st ( dom F) = X & F is one-to-one holds ex XF be XFinSequence of INT st ( dom XF) = ( card X) & ((( card X) ! ) - ( Sum XF)) = ( card { h where h be Function of X, ( rng F) : h is one-to-one & for x st x in X holds (h . x) <> (F . x) }) & for n st n in ( dom XF) holds (XF . n) = (((( - 1) |^ n) * (( card X) ! )) / ((n + 1) ! ))

    proof

      let X, Y;

      let F be Function of X, Y such that

       A1: ( dom F) = X and

       A2: F is one-to-one;

      deffunc fy( object) = { h where h be Function of X, ( rng F) : h is one-to-one & (h . $1) = (F . $1) };



       A3: for x be object st x in X holds fy(x) in ( bool ( Funcs (X,( rng F))))

      proof

        let x be object such that

         A4: x in X;

         fy(x) c= ( Funcs (X,( rng F)))

        proof

          let y be object;

          assume y in fy(x);

          then

           A5: ex h be Function of X, ( rng F) st y = h & h is one-to-one & (h . x) = (F . x);

          ( rng F) <> {} by A1, A4, RELAT_1: 42;

          hence thesis by A5, FUNCT_2: 8;

        end;

        hence thesis;

      end;

      consider Fy9 be Function of X, ( bool ( Funcs (X,( rng F)))) such that

       A6: for x be object st x in X holds (Fy9 . x) = fy(x) from FUNCT_2:sch 2( A3);

      defpred xf[ object, object] means for n, k st n = $1 & k = (( card X) - (n + 1)) holds $2 = (k ! );



       A7: for x be object st x in ( Segm ( card X)) holds ex y be object st y in NAT & xf[x, y]

      proof

        let x be object such that

         A8: x in ( Segm ( card X));

        reconsider n = x as Element of NAT by A8;

        n < ( card X) by A8, NAT_1: 44;

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

        then

        reconsider k = (( card X) - (n + 1)) as Element of NAT by NAT_1: 21;

         xf[n, (k ! )];

        hence thesis;

      end;

      consider XF be Function of ( Segm ( card X)), NAT such that

       A9: for x be object st x in ( Segm ( card X)) holds xf[x, (XF . x)] from FUNCT_2:sch 1( A7);

      for y be object st y in ( dom Fy9) holds (Fy9 . y) is finite

      proof

        let y be object;

        assume y in ( dom Fy9);

        then (Fy9 . y) in ( rng Fy9) by FUNCT_1:def 3;

        hence thesis;

      end;

      then

      reconsider Fy = Fy9 as finite-yielding Function by FINSET_1:def 4;

      reconsider rngF = ( rng F) as finite set;



       A10: ( dom XF) = ( card X) by FUNCT_2:def 1;

      then

      reconsider XF as XFinSequence by AFINSQ_1: 5;

      reconsider XF as XFinSequence of NAT ;



       A11: for n st n in ( dom XF) holds ex x, y st x <> y & for f st f in ( Choose (X,(n + 1),x,y)) holds ( card ( Intersection (Fy,f,x))) = (XF . n)

      proof

        let n such that

         A12: n in ( dom XF);

        n < ( len XF) by A12, AFINSQ_1: 86;

        then n < ( card X) by A10;

        then

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

        then

        reconsider c = (( card X) - (n + 1)) as Element of NAT by NAT_1: 21;



         A14: (( card X) -' (n + 1)) = c by A13, XREAL_1: 233;

        take 0 , 1;

        thus 0 <> 1;

        let f9 be Function;

        assume f9 in ( Choose (X,(n + 1), 0 ,1));

        then

        consider f be Function of X, { 0 , 1} such that

         A15: f = f9 and

         A16: ( card (f " { 0 })) = (n + 1) by Def1;

        reconsider f0 = (f " { 0 }) as finite set;

        set Xf0 = (X \ f0);

        set S = { h where h be Function of X, rngF : h is one-to-one & ( rng (h | Xf0)) c= (F .: Xf0) & for x st x in f0 holds (h . x) = (F . x) };



         A17: ( Intersection (Fy,f, 0 )) c= S

        proof

          assume not ( Intersection (Fy,f, 0 )) c= S;

          then

          consider z be object such that

           A18: z in ( Intersection (Fy,f, 0 )) and

           A19: not z in S;

          consider x9 be object such that

           A20: x9 in (f " { 0 }) by A16, CARD_1: 27, XBOOLE_0:def 1;

          (f . x9) in { 0 } by A20, FUNCT_1:def 7;

          then

           A21: (f . x9) = 0 by TARSKI:def 1;

          x9 in ( dom f) by A20, FUNCT_1:def 7;

          then 0 in ( rng f) by A21, FUNCT_1:def 3;

          then

          consider x such that

           A22: x in ( dom f) and (f . x) = 0 and

           A23: z in (Fy . x) by A18, Th21;

          z in fy(x) by A6, A22, A23;

          then

          consider h be Function of X, ( rng F) such that

           A24: z = h and

           A25: h is one-to-one and (h . x) = (F . x);



           A26: for x1 st x1 in f0 holds (h . x1) = (F . x1)

          proof

            let x1 such that

             A27: x1 in f0;

            (f . x1) in { 0 } by A27, FUNCT_1:def 7;

            then

             A28: (f . x1) = 0 by TARSKI:def 1;

            (Fy9 . x1) = fy(x1) & x1 in ( dom f) by A6, A27, FUNCT_1:def 7;

            then h in fy(x1) by A18, A24, A28, Def2;

            then ex h9 be Function of X, ( rng F) st h = h9 & h9 is one-to-one & (h9 . x1) = (F . x1);

            hence thesis;

          end;

          ( rng (h | Xf0)) c= (F .: Xf0)

          proof

            assume not ( rng (h | Xf0)) c= (F .: Xf0);

            then

            consider y be object such that

             A29: y in ( rng (h | Xf0)) and

             A30: not y in (F .: Xf0);

            consider x1 be object such that

             A31: x1 in ( dom (h | Xf0)) and

             A32: ((h | Xf0) . x1) = y by A29, FUNCT_1:def 3;



             A33: (h . x1) = y by A31, A32, FUNCT_1: 47;

            x1 in (( dom h) /\ Xf0) by A31, RELAT_1: 61;

            then

             A34: x1 in Xf0 by XBOOLE_0:def 4;



             A35: (F .: (X \ Xf0)) = ((F .: X) \ (F .: Xf0)) by A2, FUNCT_1: 64;

            rngF = (F .: X) by A1, RELAT_1: 113;

            then y in ((F .: X) \ (F .: Xf0)) by A29, A30, XBOOLE_0:def 5;

            then

            consider x2 be object such that

             A36: x2 in ( dom F) and

             A37: x2 in (X \ Xf0) and

             A38: y = (F . x2) by A35, FUNCT_1:def 6;

            y in ( rng F) by A36, A38, FUNCT_1:def 3;

            then

             A39: X = ( dom h) by FUNCT_2:def 1;

            (X \ Xf0) = (X /\ (f " { 0 })) by XBOOLE_1: 48;

            then x2 in (f " { 0 }) by A37, XBOOLE_0:def 4;

            then

             A40: (h . x2) = y by A26, A38;

             not x2 in Xf0 by A37, XBOOLE_0:def 5;

            hence contradiction by A25, A36, A40, A33, A39, A34;

          end;

          hence thesis by A19, A24, A25, A26;

        end;



         A41: (X,rngF) are_equipotent by A1, A2, WELLORD2:def 4;

        then

         A42: ( card rngF) = ( card X) by CARD_1: 5;

        ( card rngF) = ( card X) by A41, CARD_1: 5;

        then

         A43: rngF = {} implies X is empty;



         A44: F is Function of X, rngF by A1, FUNCT_2: 1;

        S c= ( Intersection (Fy,f, 0 ))

        proof

          assume not S c= ( Intersection (Fy,f, 0 ));

          then

          consider z be object such that

           A45: z in S and

           A46: not z in ( Intersection (Fy,f, 0 ));

          consider h be Function of X, ( rng F) such that

           A47: h = z and

           A48: h is one-to-one and ( rng (h | Xf0)) c= (F .: Xf0) and

           A49: for x st x in f0 holds (h . x) = (F . x) by A45;

          consider x be object such that

           A50: x in (f " { 0 }) by A16, CARD_1: 27, XBOOLE_0:def 1;

          x in X by A50;

          then x in ( dom Fy9) by FUNCT_2:def 1;

          then

           A51: (Fy9 . x) in ( rng Fy9) by FUNCT_1:def 3;



           A52: (Fy9 . x) = fy(x) by A6, A50;

          (h . x) = (F . x) by A49, A50;

          then h in (Fy9 . x) by A48, A52;

          then h in ( union ( rng Fy9)) by A51, TARSKI:def 4;

          then

          consider y such that

           A53: y in ( dom f) and

           A54: (f . y) = 0 and

           A55: not h in (Fy . y) by A46, A47, Def2;

          (f . y) in { 0 } by A54, TARSKI:def 1;

          then y in (f " { 0 }) by A53, FUNCT_1:def 7;

          then (h . y) = (F . y) by A49;

          then h in fy(y) by A48;

          hence contradiction by A6, A53, A55;

        end;

        then S = ( Intersection (Fy,f, 0 )) by A17;

        then ( card ( Intersection (Fy,f, 0 ))) = ((( card X) -' (n + 1)) ! ) by A2, A16, A43, A44, A42, Th60;

        hence thesis by A9, A10, A12, A15, A14;

      end;



       A56: (X,rngF) are_equipotent by A1, A2, WELLORD2:def 4;

      then ( card rngF) = ( card X) by CARD_1: 5;

      then

       A57: ((( card rngF) -' ( card X)) ! ) = 1 & ( card { f where f be Function of X, rngF : f is one-to-one }) = ((( card rngF) ! ) / ((( card rngF) -' ( card X)) ! )) by Th6, NEWTON: 12, XREAL_1: 232;

      then

      reconsider One = { f where f be Function of X, ( rng F) : f is one-to-one } as finite set;

      set S = { h where h be Function of X, ( rng F) : h is one-to-one & for x st x in X holds (h . x) <> (F . x) };

      ( dom XF) = ( card X) & ( dom Fy) = X by FUNCT_2:def 1;

      then

      consider F9 be XFinSequence of INT such that

       A58: ( dom F9) = ( card X) and

       A59: ( card ( union ( rng Fy))) = ( Sum F9) and

       A60: for n st n in ( dom F9) holds (F9 . n) = (((( - 1) |^ n) * (XF . n)) * (( card X) choose (n + 1))) by A11, Th57;



       A61: ( union ( rng Fy9)) c= One

      proof

        let x be object;

        assume x in ( union ( rng Fy9));

        then

        consider Fyx be set such that

         A62: x in Fyx and

         A63: Fyx in ( rng Fy9) by TARSKI:def 4;

        consider x1 be object such that

         A64: x1 in ( dom Fy9) & (Fy . x1) = Fyx by A63, FUNCT_1:def 3;

        x in fy(x1) by A6, A62, A64;

        then ex h be Function of X, ( rng F) st h = x & h is one-to-one & (h . x1) = (F . x1);

        hence thesis;

      end;

      reconsider u = ( union ( rng Fy)) as finite set;



       A65: ( card (One \ u)) = (( card One) - ( card u)) by A61, CARD_2: 44;

      take F9;

      thus ( dom F9) = ( card X) by A58;



       A66: (One \ ( union ( rng Fy))) c= S

      proof

        let x be object such that

         A67: x in (One \ ( union ( rng Fy)));

        x in One by A67;

        then

        consider f be Function of X, ( rng F) such that

         A68: f = x and

         A69: f is one-to-one;

        assume not x in S;

        then

        consider x such that

         A70: x in X and

         A71: (f . x) = (F . x) by A68, A69;

        x in ( dom Fy) by A70, FUNCT_2:def 1;

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

        then

         A72: fy(x) in ( rng Fy) by A6, A70;

        f in fy(x) by A69, A71;

        then f in ( union ( rng Fy)) by A72, TARSKI:def 4;

        hence thesis by A67, A68, XBOOLE_0:def 5;

      end;



       A73: S c= (One \ ( union ( rng Fy)))

      proof

        let x be object;

        assume x in S;

        then

        consider f be Function of X, ( rng F) such that

         A74: x = f and

         A75: f is one-to-one and

         A76: for x st x in X holds (f . x) <> (F . x);

        assume

         A77: not x in (One \ ( union ( rng Fy)));

        f in One by A75;

        then f in ( union ( rng Fy)) by A74, A77, XBOOLE_0:def 5;

        then

        consider Fyy be set such that

         A78: f in Fyy and

         A79: Fyy in ( rng Fy) by TARSKI:def 4;

        consider y be object such that

         A80: y in ( dom Fy) and

         A81: (Fy . y) = Fyy by A79, FUNCT_1:def 3;

        y in X by A80, FUNCT_2:def 1;

        then f in fy(y) by A6, A78, A81;

        then

         A82: ex g be Function of X, ( rng F) st f = g & g is one-to-one & (g . y) = (F . y);

        y in X by A80, FUNCT_2:def 1;

        hence contradiction by A76, A82;

      end;

      ( card One) = (( card X) ! ) by A56, A57, CARD_1: 5;

      hence ( card S) = ((( card X) ! ) - ( Sum F9)) by A59, A66, A73, A65, XBOOLE_0:def 10;

      let n such that

       A83: n in ( dom F9);

      n < ( len F9) by A83, AFINSQ_1: 86;

      then n < ( card X) by A58;

      then

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

      then

      reconsider c = (( card X) - (n + 1)) as Element of NAT by NAT_1: 21;



       A85: (( card X) choose (n + 1)) = ((( card X) ! ) / ((c ! ) * ((n + 1) ! ))) by A84, NEWTON:def 3;

      (XF . n) = (c ! ) by A9, A58, A83;



      then

       A87: ((XF . n) * (( card X) choose (n + 1))) = (((c ! ) * (( card X) ! )) / ((c ! ) * ((n + 1) ! ))) by A85, XCMPLX_1: 74

      .= ((( card X) ! ) * ((c ! ) / ((c ! ) * ((n + 1) ! )))) by XCMPLX_1: 74

      .= ((( card X) ! ) * (((c ! ) / (c ! )) / ((n + 1) ! ))) by XCMPLX_1: 78

      .= ((( card X) ! ) * (1 / ((n + 1) ! ))) by XCMPLX_1: 60

      .= (((( card X) ! ) * 1) / ((n + 1) ! )) by XCMPLX_1: 74;

      (F9 . n) = (((( - 1) |^ n) * (XF . n)) * (( card X) choose (n + 1))) by A60, A83

      .= ((( - 1) |^ n) * ((( card X) ! ) / ((n + 1) ! ))) by A87;

      hence thesis by XCMPLX_1: 74;

    end;

    theorem :: CARD_FIN:62



     Th61: for F be Function st ( dom F) = X & F is one-to-one holds ex XF be XFinSequence of INT st ( Sum XF) = ( card { h where h be Function of X, ( rng F) : h is one-to-one & for x st x in X holds (h . x) <> (F . x) }) & ( dom XF) = (( card X) + 1) & for n st n in ( dom XF) holds (XF . n) = (((( - 1) |^ n) * (( card X) ! )) / (n ! ))

    proof

      let F9 be Function such that

       A1: ( dom F9) = X and

       A2: F9 is one-to-one;

      (X,( rng F9)) are_equipotent by A1, A2, WELLORD2:def 4;

      then ( card X) = ( card ( rng F9)) by CARD_1: 5;

      then

      reconsider rngF = ( rng F9) as finite set;

      reconsider F = F9 as Function of X, rngF by A1, FUNCT_2: 1;

      set S = { h where h be Function of X, ( rng F9) : h is one-to-one & for x st x in X holds (h . x) <> (F9 . x) };

      ( rng F9) = ( rng F);

      then

      consider Xf be XFinSequence of INT such that

       A3: ( dom Xf) = ( card X) and

       A4: ((( card X) ! ) - ( Sum Xf)) = ( card S) and

       A5: for n st n in ( dom Xf) holds (Xf . n) = (((( - 1) |^ n) * (( card X) ! )) / ((n + 1) ! )) by A1, A2, Lm4;

      reconsider c = (( card X) ! ) as Element of INT by INT_1:def 2;



       A6: ( len <%c%>) = 1 by AFINSQ_1: 33;

      set F1 = (( - 1) (#) Xf);



       A7: ( dom F1) = ( card X) by A3, VALUED_1:def 5;

      reconsider F1 as XFinSequence of INT ;

      set XF = ( <%c%> ^ F1);

      take XF;

      (( - 1) * ( Sum Xf)) = ( Sum F1) by AFINSQ_2: 64;



      then (c - ( Sum Xf)) = (c + ( Sum F1))

      .= ( addint . (c,( Sum F1))) by BINOP_2:def 20

      .= ( addint . (( addint "**" <%c%>),( Sum F1))) by AFINSQ_2: 37

      .= ( addint . (( addint "**" <%c%>),( addint "**" F1))) by AFINSQ_2: 50

      .= ( addint "**" XF) by AFINSQ_2: 42

      .= ( Sum XF) by AFINSQ_2: 50;

      hence ( Sum XF) = ( card S) by A4;

      ( len F1) = ( card X) by A3, VALUED_1:def 5;

      hence

       A8: ( dom XF) = (( card X) + 1) by A6, AFINSQ_1:def 3;

      let n such that

       A9: n in ( dom XF);

      per cases ;

        suppose

         A10: n = 0 ;

        then (( - 1) |^ n) = 1 by NEWTON: 4;

        hence thesis by A10, AFINSQ_1: 35, NEWTON: 12;

      end;

        suppose n > 0 ;

        then

        reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

        (n1 + 1) = n;

        then

         A11: (( - 1) * (( - 1) |^ n1)) = (( - 1) |^ n) by NEWTON: 6;

        n < ( len XF) by A9, AFINSQ_1: 86;

        then n < (( card X) + 1) by A8;

        then (n1 + 1) <= ( card X) by NAT_1: 13;

        then n1 < ( len F1) by A7, NAT_1: 13;

        then

         A12: n1 in ( dom F1) by AFINSQ_1: 86;

        ( len <%c%>) = 1 by AFINSQ_1: 33;

        then (XF . (n1 + 1)) = (F1 . n1) by A12, AFINSQ_1:def 3;

        then

         A13: (XF . (n1 + 1)) = (( - 1) * (Xf . n1)) by VALUED_1: 6;

        (Xf . n1) = (((( - 1) |^ n1) * (( card X) ! )) / ((n1 + 1) ! )) by A3, A5, A7, A12;

        then (XF . n) = ((( - 1) * ((( - 1) |^ n1) * (( card X) ! ))) / (n ! )) by A13, XCMPLX_1: 74;

        hence thesis by A11;

      end;

    end;

    theorem :: CARD_FIN:63

    ex XF be XFinSequence of INT st ( Sum XF) = ( card { h where h be Function of X, X : h is one-to-one & for x st x in X holds (h . x) <> x }) & ( dom XF) = (( card X) + 1) & for n st n in ( dom XF) holds (XF . n) = (((( - 1) |^ n) * (( card X) ! )) / (n ! ))

    proof

      set S1 = { h where h be Function of X, X : h is one-to-one & for x st x in X holds (h . x) <> (( id X) . x) };

      set S2 = { h where h be Function of X, X : h is one-to-one & for x st x in X holds (h . x) <> x };



       A1: S2 c= S1

      proof

        let x be object;

        assume x in S2;

        then

        consider h be Function of X, X such that

         A2: h = x & h is one-to-one and

         A3: for y st y in X holds (h . y) <> y;

        for y st y in X holds (( id X) . y) <> (h . y) by A3, FUNCT_1: 17;

        hence thesis by A2;

      end;



       A4: ( dom ( id X)) = X & ( rng ( id X)) = X;

      S1 c= S2

      proof

        let x be object;

        assume x in S1;

        then

        consider h be Function of X, X such that

         A5: h = x & h is one-to-one and

         A6: for y st y in X holds (h . y) <> (( id X) . y);

        now

          let y such that

           A7: y in X;

          (( id X) . y) = y by A7, FUNCT_1: 17;

          hence (h . y) <> y by A6, A7;

        end;

        hence thesis by A5;

      end;

      then S1 = S2 by A1;

      hence thesis by A4, Th61;

    end;