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 A1: ( ( Y1 is empty implies X1 is empty ) & 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 ) ) }
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 A2: ( F is one-to-one & 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 ) ) }
set XX = X1 \ X;
defpred S₁[ Function, set , set ] means ( $1 is one-to-one & rng ($1 | (X1 \ X)) = F .: (X1 \ X) );
deffunc H₁( set ) -> set = F . $1;
A3: for x being set st x in X1 \ (X1 \ X) holds
H₁(x) in Y1

proof

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

end;

A5: ( X1 \ X c= X1 & F .: (X1 \ X) c= Y1 ) ;
then X1 \ X c= dom F by A1, FUNCT_2:def 1;
then A6: ( F .: (X1 \ X) is empty implies X1 \ X is empty ) by RELAT_1:152;
A7: 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 A8: 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:84, RELAT_1:101; :: 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

assume A9: S₁[f | (X1 \ X),X1 \ X,F .: (X1 \ X)] ; :: thesis: S₁[f,X1,Y1]
f | (X1 \ (X1 \ X)) = F | (X1 \ (X1 \ X))

proof

A10: ( dom (f | (X1 \ (X1 \ X))) = (dom f) /\ (X1 \ (X1 \ X)) & dom f = X1 & dom (F | (X1 \ (X1 \ X))) = (dom F) /\ (X1 \ (X1 \ X)) & dom F = X1 ) by A1, FUNCT_2:def 1, RELAT_1:90;

now

let x be set ; :: thesis: ( x in dom (F | (X1 \ (X1 \ X))) implies F . x = (f | (X1 \ (X1 \ X))) . x )
assume A11: x in dom (F | (X1 \ (X1 \ X))) ; :: thesis: F . x = (f | (X1 \ (X1 \ X))) . x
( X1 \ (X1 \ X) = X /\ X1 & X /\ X1 = X ) by A1, XBOOLE_1:28, XBOOLE_1:48;
then ( f . x = (f | (X1 \ (X1 \ X))) . x & F . x = f . x ) by A8, A10, A11, FUNCT_1:70;
hence F . x = (f | (X1 \ (X1 \ X))) . x ; :: thesis: verum

end;

hence f | (X1 \ (X1 \ X)) = F | (X1 \ (X1 \ X)) by A10, FUNCT_1:68; :: thesis: verum

end;

then ( rng (f | (X1 \ (X1 \ X))) = F .: (X1 \ (X1 \ X)) & rng (f | (X1 \ X)) = F .: (X1 \ X) & (X1 \ (X1 \ X)) \/ (X1 \ X) = X1 & rng (f | (X1 \ (X1 \ X))) = f .: (X1 \ (X1 \ X)) & rng (f | (X1 \ X)) = f .: (X1 \ X) & F .: ((X1 \ (X1 \ X)) \/ (X1 \ X)) = (F .: (X1 \ (X1 \ X))) \/ (F .: (X1 \ X)) & f .: ((X1 \ (X1 \ X)) \/ (X1 \ X)) = (f .: (X1 \ (X1 \ X))) \/ (f .: (X1 \ X)) ) by A9, RELAT_1:101, RELAT_1:148, RELAT_1:153, XBOOLE_1:45;
then ( F .: X1 = f .: X1 & X1 = dom F & X1 = dom f & F is onto & F .: (dom F) = rng F ) by A1, A2, FUNCT_2:def 1, RELAT_1:146, STIRL2_1:70;
then ( rng F = rng f & rng F = Y1 ) by FUNCT_2:def 3, RELAT_1:146;
then f is onto by FUNCT_2:def 3;
hence S₁[f,X1,Y1] by A2, A9, RELAT_1:101, STIRL2_1:70; :: thesis: verum

end;

end;

set S1 = { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ 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) ) ) } ;
set F1 = { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } ;
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 ) ) } ;
dom F = X1 by A1, FUNCT_2:def 1;
then X1 \ X,F .: (X1 \ X) are_equipotent by A2, CARD_1:60;
then A12: card (X1 \ X) = card (F .: (X1 \ X)) by CARD_1:21;
reconsider FX = F .: (X1 \ X) as finite set ;
A13: { 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 set ; :: 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 A14: 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 }
ex f being Function of (X1 \ X),FX st
( f = x & S₁[f,X1 \ X,F .: (X1 \ X)] ) by A14;
hence x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } ; :: thesis: verum

end;

A15: { 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 set ; :: 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 A16: 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)] }
consider f being Function of (X1 \ X),FX such that
A17: ( x = f & f is one-to-one ) by A16;
( FX = {} implies X1 \ X = {} ) by A12;
then ( f is onto & dom f = X1 \ X ) by A12, A17, FUNCT_2:def 1, STIRL2_1:70;
then ( rng f = FX & f | (X1 \ X) = f ) by FUNCT_2:def 3, RELAT_1:98;
hence x in { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : S₁[f,X1 \ X,F .: (X1 \ X)] } by A17; :: thesis: verum

end;

A18: ( X1 \ (X1 \ X) = X /\ X1 & X /\ X1 = X ) by A1, XBOOLE_1:28, XBOOLE_1:48;
A19: { 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 set ; :: 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 A20: 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 ) ) }
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) ) ) by A20;
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 A18; :: thesis: verum

end;

A21: { 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 set ; :: 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 A22: 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) ) ) }
consider f being Function of X1,Y1 such that
A23: ( x = f & f is one-to-one ) and
A24: rng (f | (X1 \ X)) c= F .: (X1 \ X) and
A25: for x being set st x in X holds
f . x = F . x by A22;
dom f = X1 by A1, FUNCT_2:def 1;
then X1 \ X,f .: (X1 \ X) are_equipotent by A23, CARD_1:60;
then card (X1 \ X) = card (f .: (X1 \ X)) by CARD_1:21;
then card FX = card (rng (f | (X1 \ X))) by A12, RELAT_1:148;
then rng (f | (X1 \ X)) = FX by A24, TRIANG_1:3;
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 A18, A23, A25; :: thesis: verum

end;

( 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 & card (X1 \ X) = (card X1) - (card X) & card (X1 \ X) >= 0 ) by A1, A12, Th7, CARD_2:63, XREAL_1:234;
then A26: ( card { f where f is Function of (X1 \ X),(F .: (X1 \ X)) : f is one-to-one } = ((card X1) -' (card X)) ! & { 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)] } & { 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 ) ) } = { 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 A13, A15, A19, A21, NEWTON:18, XBOOLE_0:def 10, XREAL_0:def 2;
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(A3, A5, A6, A7);
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 A26; :: thesis: verum