let X be finite set ; for k being Nat
for z, x, y being object st x <> y & not z in X holds
card (Choose ((X \/ {z}),(k + 1),x,y)) = (card (Choose (X,(k + 1),x,y))) + (card (Choose (X,k,x,y)))
let k be Nat; for z, x, y being object st x <> y & not z in X holds
card (Choose ((X \/ {z}),(k + 1),x,y)) = (card (Choose (X,(k + 1),x,y))) + (card (Choose (X,k,x,y)))
let z, x, y be object ; ( x <> y & not z in X implies card (Choose ((X \/ {z}),(k + 1),x,y)) = (card (Choose (X,(k + 1),x,y))) + (card (Choose (X,k,x,y))) )
assume that
A1:
x <> y
and
A2:
not z in X
; card (Choose ((X \/ {z}),(k + 1),x,y)) = (card (Choose (X,(k + 1),x,y))) + (card (Choose (X,k,x,y)))
set F2 = { 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 ) } ;
A3:
{ 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)
by A1, Lm1;
( { 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} : ( 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 ) } & { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = 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 ) } )
by XBOOLE_1:7;
then reconsider F1 = { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } , F2 = { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } as finite set by A3;
A4:
card F1 = card (Choose (X,k,x,y))
by A2, Th12;
( card (F1 \/ F2) = (card F1) + (card F2) & card F2 = card (Choose (X,(k + 1),x,y)) )
by A1, A2, Lm1, Th13, CARD_2:40;
hence
card (Choose ((X \/ {z}),(k + 1),x,y)) = (card (Choose (X,(k + 1),x,y))) + (card (Choose (X,k,x,y)))
by A1, A4, Lm1; verum