let x, y, z be set ; :: thesis: for X being finite set
for k being Element of NAT 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 X be finite set ; :: thesis: for k being Element of NAT 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 Element of NAT ; :: thesis: ( 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 A1: ( x <> y & not z in X ) ; :: thesis: card (Choose (X \/ {z}),(k + 1),x,y) = (card (Choose X,(k + 1),x,y)) + (card (Choose X,k,x,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 ) } ;
( { 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 ) } 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 A1, Lm1, 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 ;
F1 misses F2 by A1, Lm1;
then ( card (F1 \/ F2) = (card F1) + (card F2) & card F2 = card (Choose X,(k + 1),x,y) & card F1 = card (Choose X,k,x,y) ) by A1, Th14, Th16, CARD_2:53;
hence card (Choose (X \/ {z}),(k + 1),x,y) = (card (Choose X,(k + 1),x,y)) + (card (Choose X,k,x,y)) by A1, Lm1; :: thesis: verum