let X be finite set ; :: thesis: for k being Nat
for z, x, y being object st x <> y holds
( { 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} : ( card (f " {x}) = k + 1 & f . z = y ) } = Choose ((X \/ {z}),(k + 1),x,y) & { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } misses { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } )
let k be Nat; :: thesis: for z, x, y being object st x <> y holds
( { 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} : ( card (f " {x}) = k + 1 & f . z = y ) } = Choose ((X \/ {z}),(k + 1),x,y) & { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } misses { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } )
let z, x, y be object ; :: thesis: ( x <> y implies ( { 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} : ( card (f " {x}) = k + 1 & f . z = y ) } = Choose ((X \/ {z}),(k + 1),x,y) & { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } misses { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } ) )
set F1 = { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } ;
set F2 = { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } ;
assume A1: x <> y ; :: thesis: ( { 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} : ( card (f " {x}) = k + 1 & f . z = y ) } = Choose ((X \/ {z}),(k + 1),x,y) & { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } misses { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } )
A2: { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } misses { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) }

proof

assume { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } meets { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } ; :: thesis: contradiction
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} : ( card (f " {x}) = k + 1 & f . z = y ) } <> {} ;
then consider x1 being object such that
A3: x1 in { 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} : ( card (f " {x}) = k + 1 & f . z = y ) } by XBOOLE_0:def 1;
x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } by A3, XBOOLE_0:def 4;
then A4: ex f2 being Function of (X \/ {z}),{x,y} st
( x1 = f2 & card (f2 " {x}) = k + 1 & f2 . z = y ) ;
x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } by A3, XBOOLE_0:def 4;
then ex f1 being Function of (X \/ {z}),{x,y} st
( x1 = f1 & card (f1 " {x}) = k + 1 & f1 . z = x ) ;
hence contradiction by A1, A4; :: thesis: verum

end;

A5: { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } c= Choose ((X \/ {z}),(k + 1),x,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 + 1 & f . z = y ) } or x1 in Choose ((X \/ {z}),(k + 1),x,y) )
assume x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } ; :: thesis: x1 in Choose ((X \/ {z}),(k + 1),x,y)
then ex f being Function of (X \/ {z}),{x,y} st
( x1 = f & card (f " {x}) = k + 1 & f . z = y ) ;
hence x1 in Choose ((X \/ {z}),(k + 1),x,y) by Def1; :: thesis: verum

end;

A6: Choose ((X \/ {z}),(k + 1),x,y) c= { 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} : ( card (f " {x}) = k + 1 & f . z = y ) }

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in Choose ((X \/ {z}),(k + 1),x,y) or x1 in { 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} : ( card (f " {x}) = k + 1 & f . z = y ) } )
assume x1 in Choose ((X \/ {z}),(k + 1),x,y) ; :: thesis: x1 in { 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} : ( card (f " {x}) = k + 1 & f . z = y ) }
then consider f being 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 { 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} : ( card (f " {x}) = k + 1 & f . z = y ) } ) by A7;
hence x1 in { 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} : ( card (f " {x}) = k + 1 & f . z = y ) } by XBOOLE_0:def 3; :: thesis: verum

end;

{ f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } c= Choose ((X \/ {z}),(k + 1),x,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 + 1 & f . z = x ) } or x1 in Choose ((X \/ {z}),(k + 1),x,y) )
assume x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } ; :: thesis: x1 in Choose ((X \/ {z}),(k + 1),x,y)
then ex f being Function of (X \/ {z}),{x,y} st
( x1 = f & card (f " {x}) = k + 1 & f . z = x ) ;
hence x1 in Choose ((X \/ {z}),(k + 1),x,y) by Def1; :: 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} : ( card (f " {x}) = k + 1 & f . z = y ) } c= Choose ((X \/ {z}),(k + 1),x,y) by A5, XBOOLE_1:8;
hence ( { 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} : ( card (f " {x}) = k + 1 & f . z = y ) } = Choose ((X \/ {z}),(k + 1),x,y) & { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } misses { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } ) by A6, A2; :: thesis: verum