let X be finite set ; :: thesis: 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; :: thesis: 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 ; :: 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 that
A1: x <> y and
A2: 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 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; :: thesis: verum