let X be finite set ; 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; 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 ; ( 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
; ( { 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 ) }
;
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;
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 ;
TARSKI:def 3 ( 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 ) }
;
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;
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 ;
TARSKI:def 3 ( 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)
;
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;
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 ;
TARSKI:def 3 ( 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 ) }
;
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;
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; verum