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

proof

let f be Function of (X \/ {z}),({x,y} \/ {y}); :: thesis: ( f . z = y implies ( S₁[f,X \/ {z},{x,y} \/ {y}] iff S₁[f | X,X,{x,y}] ) )
assume A4: f . z = y ; :: thesis: ( S₁[f,X \/ {z},{x,y} \/ {y}] iff S₁[f | X,X,{x,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 ( S₁[f,X \/ {z},{x,y} \/ {y}] iff S₁[f | X,X,{x,y}] ) ; :: thesis: verum

end;

set F2 = { f where f is Function of (X \/ {z}),({x,y} \/ {y}) : ( S₁[f,X \/ {z},{x,y} \/ {y}] & rng (f | X) c= {x,y} & f . z = y ) } ;
set F1 = { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } ;
A5: ( {x,y} is empty implies X is empty ) ;
A6: 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} \/ {y}) : ( S₁[f,X \/ {z},{x,y} \/ {y}] & rng (f | X) c= {x,y} & f . z = y ) } from STIRL2_1:sch 4(A5, A1, A3);
set F3 = { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k & f . z = y ) } ;
A7: { f where f is Function of (X \/ {z}),({x,y} \/ {y}) : ( S₁[f,X \/ {z},{x,y} \/ {y}] & rng (f | X) c= {x,y} & f . z = y ) } c= { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k & f . z = y ) }

proof

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

end;

A12: { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k & f . z = y ) } c= { f where f is Function of (X \/ {z}),({x,y} \/ {y}) : ( S₁[f,X \/ {z},{x,y} \/ {y}] & rng (f | X) c= {x,y} & f . z = y ) }

proof

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 & f . z = y ) } or x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {y}) : ( S₁[f,X \/ {z},{x,y} \/ {y}] & rng (f | X) c= {x,y} & f . z = y ) } )
assume x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k & f . z = y ) } ; :: thesis: x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {y}) : ( S₁[f,X \/ {z},{x,y} \/ {y}] & rng (f | X) c= {x,y} & f . z = y ) }
then consider f being 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;
S₁[f,X \/ {z},{x,y} \/ {y}] by A14;
hence x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {y}) : ( S₁[f,X \/ {z},{x,y} \/ {y}] & rng (f | X) c= {x,y} & f . z = y ) } by A13, A15, A16; :: thesis: verum

end;

A17: 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
A18: x1 = f and
A19: card (f " {x}) = k by Def1;
S₁[f,X,{x,y}] by A19;
hence x1 in { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } by A18; :: thesis: verum

end;

{ 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
A20: x1 = f and
A21: S₁[f,X,{x,y}] ;
card (f " {x}) = k by A21;
hence x1 in Choose (X,k,x,y) by A20, Def1; :: thesis: verum

end;

then Choose (X,k,x,y) = { f where f is Function of X,{x,y} : S₁[f,X,{x,y}] } by A17;
hence card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k & f . z = y ) } by A7, A12, A6, XBOOLE_0:def 10; :: thesis: verum