let X be finite set ; :: thesis: for k being Nat
for z, x, y being object st not z in X holds
card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
let k be Nat; :: thesis: for z, x, y being object st not z in X holds
card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
let z, x, y be object ; :: thesis: ( not z in X implies card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } )
set F1 = { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } ;
defpred S₁[ set , set , set ] means for f being Function st f = $1 holds
card ((f | X) " {x}) = k;
A1: for f being Function of (X \/ {z}),({x,y} \/ {x}) st f . z = x holds
( S₁[f,X \/ {z},{x,y} \/ {x}] iff S₁[f | X,X,{x,y}] )

proof

let f be Function of (X \/ {z}),({x,y} \/ {x}); :: thesis: ( f . z = x implies ( S₁[f,X \/ {z},{x,y} \/ {x}] iff S₁[f | X,X,{x,y}] ) )
assume f . z = x ; :: thesis: ( S₁[f,X \/ {z},{x,y} \/ {x}] iff S₁[f | X,X,{x,y}] )
f | X = (f | X) | X ;
hence ( S₁[f,X \/ {z},{x,y} \/ {x}] iff S₁[f | X,X,{x,y}] ) ; :: thesis: verum

end;

set F3 = { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } ;
set F2 = { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } ;
assume A2: not z in X ; :: thesis: card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
A3: { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } c= { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }

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 ; :: according to TARSKI:def 3 :: thesis: ( not x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } or x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } )
assume x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } ; :: thesis: x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
then consider f being Function of (X \/ {z}),({x,y} \/ {x}) such that
A6: x1 = f and
A7: S₁[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 x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } by A6, A8, A4; :: thesis: verum

end;

A11: { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } c= Choose (X,k,x,y)

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } or x1 in Choose (X,k,x,y) )
assume x1 in { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } ; :: thesis: x1 in Choose (X,k,x,y)
then consider f being Function of X,{x,y} such that
A12: x1 = f and
A13: S₁[f,X,{x,y}] ;
f | X = f ;
then card (f " {x}) = k by A13;
hence x1 in Choose (X,k,x,y) by A12, Def1; :: thesis: verum

end;

A14: Choose (X,k,x,y) c= { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] }

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in Choose (X,k,x,y) or x1 in { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } )
assume x1 in Choose (X,k,x,y) ; :: thesis: x1 in { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] }
then consider f being Function of X,{x,y} such that
A15: x1 = f and
A16: card (f " {x}) = k by Def1;
S₁[f,X,{x,y}] by A16;
hence x1 in { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } by A15; :: thesis: verum

end;

A17: ( {x,y} is empty implies X is empty ) ;
A18: card { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } = card { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } from STIRL2_1:sch 4(A17, A2, A1);
{ f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } c= { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) }

proof

z in {z} by TARSKI:def 1;
then A19: z in X \/ {z} by XBOOLE_0:def 3;
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } or x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } )
assume x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } ; :: thesis: x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) }
then consider f being 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: S₁[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 x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } by A20, A22, A24; :: thesis: verum

end;

then { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } = { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S₁[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } by A3;
hence card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } by A11, A14, A18, XBOOLE_0:def 10; :: thesis: verum