let X1, Y1, X be finite set ; :: thesis: ( ( Y1 is empty implies X1 is empty ) & X c= X1 implies for F being Function of X1,Y1 st F is one-to-one & card X1 = card Y1 holds
((card X1) -' (card X)) ! = card { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) } )
assume that
A1: ( Y1 is empty implies X1 is empty ) and
A2: X c= X1 ; :: thesis: for F being Function of X1,Y1 st F is one-to-one & card X1 = card Y1 holds
((card X1) -' (card X)) ! = card { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) }
set XX = X1 \ X;
let F be Function of X1,Y1; :: thesis: ( F is one-to-one & card X1 = card Y1 implies ((card X1) -' (card X)) ! = card { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) } )
assume that
A3: F is one-to-one and
A4: card X1 = card Y1 ; :: thesis: ((card X1) -' (card X)) ! = card { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) }
deffunc H₁( set ) -> set = F . $1;
defpred S₁[ Function, set , set ] means ( $1 is one-to-one & rng ($1 | (X1 \ X)) = F .: (X1 \ X) );
reconsider FX = F .: (X1 \ X) as finite set ;
set F1 = { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } ;
A5: card (X1 \ X) = (card X1) - (card X) by A2, CARD_2:44;
A6: for f being Function of X1,Y1 st ( for x being set st x in X1 \ (X1 \ X) holds
H₁(x) = f . x ) holds
( S₁[f,X1,Y1] iff S₁[f | (X1 \ X),X1 \ X,F .: (X1 \ X)] )

proof

let f be Function of X1,Y1; :: thesis: ( ( for x being set st x in X1 \ (X1 \ X) holds
H₁(x) = f . x ) implies ( S₁[f,X1,Y1] iff S₁[f | (X1 \ X),X1 \ X,F .: (X1 \ X)] ) )
assume A7: for x being set st x in X1 \ (X1 \ X) holds
H₁(x) = f . x ; :: thesis: ( S₁[f,X1,Y1] iff S₁[f | (X1 \ X),X1 \ X,F .: (X1 \ X)] )
thus ( S₁[f,X1,Y1] implies S₁[f | (X1 \ X),X1 \ X,F .: (X1 \ X)] ) by FUNCT_1:52; :: thesis: ( S₁[f | (X1 \ X),X1 \ X,F .: (X1 \ X)] implies S₁[f,X1,Y1] )
thus ( S₁[f | (X1 \ X),X1 \ X,F .: (X1 \ X)] implies S₁[f,X1,Y1] ) :: thesis: verum

proof

F is onto by A3, A4, FINSEQ_4:63;
then A8: rng F = Y1 by FUNCT_2:def 3;
A9: ( rng (f | (X1 \ X)) = f .: (X1 \ X) & F .: ((X1 \ (X1 \ X)) \/ (X1 \ X)) = (F .: (X1 \ (X1 \ X))) \/ (F .: (X1 \ X)) ) by RELAT_1:115, RELAT_1:120;
A10: ( dom (F | (X1 \ (X1 \ X))) = (dom F) /\ (X1 \ (X1 \ X)) & dom F = X1 ) by A1, FUNCT_2:def 1, RELAT_1:61;
A11: ( dom (f | (X1 \ (X1 \ X))) = (dom f) /\ (X1 \ (X1 \ X)) & dom f = X1 ) by A1, FUNCT_2:def 1, RELAT_1:61;

now :: thesis: for x being object st x in dom (F | (X1 \ (X1 \ X))) holds
F . x = (f | (X1 \ (X1 \ X))) . x

A12: ( X1 \ (X1 \ X) = X /\ X1 & X /\ X1 = X ) by A2, XBOOLE_1:28, XBOOLE_1:48;
let x be object ; :: thesis: ( x in dom (F | (X1 \ (X1 \ X))) implies F . x = (f | (X1 \ (X1 \ X))) . x )
assume A13: x in dom (F | (X1 \ (X1 \ X))) ; :: thesis: F . x = (f | (X1 \ (X1 \ X))) . x
f . x = (f | (X1 \ (X1 \ X))) . x by A11, A10, A13, FUNCT_1:47;
hence F . x = (f | (X1 \ (X1 \ X))) . x by A7, A10, A13, A12; :: thesis: verum

end;

then f | (X1 \ (X1 \ X)) = F | (X1 \ (X1 \ X)) by A11, A10, FUNCT_1:46;
then A14: rng (f | (X1 \ (X1 \ X))) = F .: (X1 \ (X1 \ X)) by RELAT_1:115;
A15: ( (X1 \ (X1 \ X)) \/ (X1 \ X) = X1 & rng (f | (X1 \ (X1 \ X))) = f .: (X1 \ (X1 \ X)) ) 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: S₁[f | (X1 \ X),X1 \ X,F .: (X1 \ X)] ; :: thesis: S₁[f,X1,Y1]
then rng (f | (X1 \ X)) = F .: (X1 \ X) ;
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 S₁[f,X1,Y1] by A4, A18, FINSEQ_4:63; :: thesis: verum

end;

end;

set F2 = { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) } ;
set S2 = { f where f is Function of X1,Y1 : ( S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) } ;
A19: ( X1 \ (X1 \ X) = X /\ X1 & X /\ X1 = X ) by A2, XBOOLE_1:28, XBOOLE_1:48;
A20: { f where f is Function of X1,Y1 : ( S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) } c= { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of X1,Y1 : ( S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) } or x in { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) } )
assume x in { f where f is Function of X1,Y1 : ( S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) } ; :: thesis: x in { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) }
then ex f being Function of X1,Y1 st
( x = f & S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) ;
hence x in { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) } by A19; :: thesis: verum

end;

dom F = X1 by A1, FUNCT_2:def 1;
then X1 \ X,F .: (X1 \ X) are_equipotent by A3, CARD_1:33;
then A21: card (X1 \ X) = card (F .: (X1 \ X)) by CARD_1:5;
then ( card { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } = ((card (X1 \ X)) !) / (((card FX) -' (card (X1 \ X))) !) & (card FX) -' (card (X1 \ X)) = 0 ) by Th6, XREAL_1:232;
then A22: card { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } = ((card X1) -' (card X)) ! by A5, NEWTON:12, XREAL_0:def 2;
set S1 = { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] } ;
A23: for x being set st x in X1 \ (X1 \ X) holds
H₁(x) in Y1

proof

A24: X1 = dom F by A1, FUNCT_2:def 1;
let x be set ; :: thesis: ( x in X1 \ (X1 \ X) implies H₁(x) in Y1 )
assume x in X1 \ (X1 \ X) ; :: thesis: H₁(x) in Y1
then F . x in rng F by A24, FUNCT_1:def 3;
hence H₁(x) in Y1 ; :: thesis: verum

end;

A25: { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } c= { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } or x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] } )
assume x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } ; :: thesis: x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] }
then consider f being Function of (X1 \ X),FX such that
A26: x = f and
A27: f is one-to-one ;
A28: f | (X1 \ X) = f ;
f is onto by A21, A27, FINSEQ_4:63;
then rng f = FX by FUNCT_2:def 3;
hence x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] } by A26, A27, A28; :: thesis: verum

end;

{ f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] } c= { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] } or x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } )
assume x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] } ; :: thesis: x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one }
then ex f being Function of (X1 \ X),FX st
( f = x & S₁[f,X1 \ X,F .: (X1 \ X)] ) ;
hence x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } ; :: thesis: verum

end;

then A29: { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } = { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] } by A25;
A30: { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) } c= { f where f is Function of X1,Y1 : ( S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) } or x in { f where f is Function of X1,Y1 : ( S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) } )
assume x in { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) } ; :: thesis: x in { f where f is Function of X1,Y1 : ( S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) }
then consider f being Function of X1,Y1 such that
A31: x = f and
A32: f is one-to-one and
A33: rng (f | (X1 \ X)) c= F .: (X1 \ X) and
A34: for x being set st x in X holds
f . x = F . x ;
dom f = X1 by A1, FUNCT_2:def 1;
then X1 \ X,f .: (X1 \ X) are_equipotent by A32, CARD_1:33;
then card (X1 \ X) = card (f .: (X1 \ X)) by CARD_1:5;
then card FX = card (rng (f | (X1 \ X))) by A21, RELAT_1:115;
then rng (f | (X1 \ X)) = FX by A33, CARD_2:102;
hence x in { f where f is Function of X1,Y1 : ( S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) } by A19, A31, A32, A34; :: thesis: verum

end;

A35: ( X1 \ X c= X1 & F .: (X1 \ X) c= Y1 ) ;
then X1 \ X c= dom F by A1, FUNCT_2:def 1;
then A36: ( F .: (X1 \ X) is empty implies X1 \ X is empty ) by RELAT_1:119;
card { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] } = card { f where f is Function of X1,Y1 : ( S₁[f,X1,Y1] & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X1 \ (X1 \ X) holds
f . x = H₁(x) ) ) } from STIRL2_1:sch 3(A23, A35, A36, A6);
hence ((card X1) -' (card X)) ! = card { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) ) } by A20, A30, A22, A29, XBOOLE_0:def 10; :: thesis: verum