let k be Element of NAT ; :: thesis:
let Fy be finite-yielding Function; :: thesis:
let X be finite set ; :: thesis:
let x be set ; :: thesis:
let n be Element of NAT ; :: thesis:
assume that
A1: ( dom Fy = X & x in dom Fy ) and
A2: k > 0 ; :: thesis:
set Xx = X \ {x};
set X0 = { f where f is Function of ((X \ {x}) \/ {x}),{1,0 } : ( card (f " {1}) = k + 1 & f . x = 0 ) } ;
set X1 = { f where f is Function of ((X \ {x}) \/ {x}),{1,0 } : ( card (f " {1}) = k + 1 & f . x = 1 ) } ;
not x in X \ {x} by ZFMISC_1:64;
then { f where f is Function of ((X \ {x}) \/ {x}),{1,0 } : ( card (f " {1}) = k + 1 & f . x = 0 ) } \/ { f where f is Function of ((X \ {x}) \/ {x}),{1,0 } : ( card (f " {1}) = k + 1 & f . x = 1 ) } = Choose ((X \ {x}) \/ {x}),(k + 1),1,0 by Lm1;
then reconsider X0 = { f where f is Function of ((X \ {x}) \/ {x}),{1,0 } : ( card (f " {1}) = k + 1 & f . x = 0 ) } , X1 = { f where f is Function of ((X \ {x}) \/ {x}),{1,0 } : ( card (f " {1}) = k + 1 & f . x = 1 ) } as finite set by FINSET_1:13, XBOOLE_1:7;
consider P0 being Function of (card X0),X0 such that
A3: P0 is one-to-one by Lm3;
defpred S₁[ set , set ] means ex f being Function st
( f = P0 . $1 & f in X0 & $2 = f | (X \ {x}) );
A4: for x0 being set st x0 in card X0 holds
ex P0x0 being set st
( P0x0 in Choose (X \ {x}),(k + 1),1,0 & S₁[x0,P0x0] )

proof

let x0 be set ; :: thesis:
assume A5: x0 in card X0 ; :: thesis:
x0 in dom P0 by A5, CARD_1:47, FUNCT_2:def 1;
then A6: P0 . x0 in rng P0 by FUNCT_1:def 5;
then P0 . x0 in X0 ;
then consider P0x0 being Function of ((X \ {x}) \/ {x}),{1,0 } such that
A7: ( P0 . x0 = P0x0 & card (P0x0 " {1}) = k + 1 & P0x0 . x = 0 ) ;
X \ {x} c= (X \ {x}) \/ {x} by XBOOLE_1:7;
then A8: ( ((X \ {x}) \/ {x}) /\ (X \ {x}) = X \ {x} & dom P0x0 = (X \ {x}) \/ {x} & rng (P0x0 | (X \ {x})) c= rng P0x0 ) by FUNCT_2:def 1, RELAT_1:99, XBOOLE_1:28;
then ( dom (P0x0 | (X \ {x})) = X \ {x} & rng (P0x0 | (X \ {x})) c= {1,0 } ) by RELAT_1:90;
then reconsider Px = P0x0 | (X \ {x}) as Function of (X \ {x}),{1,0 } by FUNCT_2:4;
not x in X \ {x} by ZFMISC_1:64;
then ((X \ {x}) \/ {x}) \ {x} = X \ {x} by ZFMISC_1:141;
then P0x0 " {1} = Px " {1} by A7, A8, Th15;
then Px in Choose (X \ {x}),(k + 1),1,0 by A7, Def1;
hence ex P0x0 being set st
( P0x0 in Choose (X \ {x}),(k + 1),1,0 & S₁[x0,P0x0] ) by A6, A7; :: thesis:

end;

consider P0x being Function of (card X0),(Choose (X \ {x}),(k + 1),1,0 ) such that
A9: for x1 being set st x1 in card X0 holds
S₁[x1,P0x . x1] from FUNCT_2:sch 1(A4);
not x in X \ {x} by ZFMISC_1:64;
then A10: card (Choose (X \ {x}),(k + 1),1,0 ) = card X0 by Th16;
for x1, x2 being set st x1 in dom P0x & x2 in dom P0x & P0x . x1 = P0x . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
assume A11: ( x1 in dom P0x & x2 in dom P0x & P0x . x1 = P0x . x2 ) ; :: thesis:
( ( Choose (X \ {x}),(k + 1),1,0 = {} implies card (Choose (X \ {x}),(k + 1),1,0 ) = {} ) & ( X0 = {} implies card X0 = {} ) ) ;
then A12: ( dom P0x = card X0 & dom P0 = card X0 ) by A10, FUNCT_2:def 1;
consider f1 being Function such that
A13: ( f1 = P0 . x1 & f1 in X0 & P0x . x1 = f1 | (X \ {x}) ) by A9, A11;
consider f2 being Function such that
A14: ( f2 = P0 . x2 & f2 in X0 & P0x . x2 = f2 | (X \ {x}) ) by A9, A11;
A15: ( ex F being Function of ((X \ {x}) \/ {x}),{1,0 } st
( f1 = F & card (F " {1}) = k + 1 & F . x = 0 ) & ex F being Function of ((X \ {x}) \/ {x}),{1,0 } st
( f2 = F & card (F " {1}) = k + 1 & F . x = 0 ) ) by A13, A14;
then A16: ( dom f1 = (X \ {x}) \/ {x} & f1 . x = 0 & dom f2 = (X \ {x}) \/ {x} & f2 . x = 0 ) by FUNCT_2:def 1;
for z being set st z in dom f1 holds
f1 . z = f2 . z

proof

let z be set ; :: thesis:
assume A17: z in dom f1 ; :: thesis:

now

per cases by A16, A17, XBOOLE_0:def 3;

suppose z in X \ {x} ; :: thesis:

then ( z in (dom f1) /\ (X \ {x}) & z in (dom f2) /\ (X \ {x}) ) by A16, A17, XBOOLE_0:def 4;
then ( (f1 | (X \ {x})) . z = f1 . z & (f2 | (X \ {x})) . z = f2 . z ) by FUNCT_1:71;
hence f1 . z = f2 . z by A11, A13, A14; :: thesis:

end;

suppose z in {x} ; :: thesis:

then z = x by TARSKI:def 1;
hence f1 . z = f2 . z by A15; :: thesis:

end;

hence f1 . z = f2 . z ; :: thesis:

end;

then ( f1 = f2 & x1 in dom P0 & x2 in dom P0 ) by A11, A12, A16, FUNCT_1:9;
hence x1 = x2 by A3, A13, A14, FUNCT_1:def 8; :: thesis:

end;

then A18: P0x is one-to-one by FUNCT_1:def 8;
(X \ {x}) /\ X = X \ {x} by XBOOLE_1:28;
then A19: dom (Fy | ((dom Fy) \ {x})) = X \ {x} by A1, RELAT_1:90;
then consider XFS0 being XFinSequence of such that
A20: dom XFS0 = dom P0x and
A21: for z being set
for f being Function st z in dom XFS0 & f = P0x . z holds
XFS0 . z = card (Intersection (Fy | ((dom Fy) \ {x})),f,1) and
A22: Card_Intersection (Fy | ((dom Fy) \ {x})),(k + 1) = Sum XFS0 by A10, A18, Def4;
consider P1 being Function of (card X1),X1 such that
A23: P1 is one-to-one by Lm3;
defpred S₂[ set , set ] means ex f being Function st
( f = P1 . $1 & f in X1 & $2 = f | (X \ {x}) );
A24: for x1 being set st x1 in card X1 holds
ex P1x1 being set st
( P1x1 in Choose (X \ {x}),k,1,0 & S₂[x1,P1x1] )

proof

let x1 be set ; :: thesis:
assume A25: x1 in card X1 ; :: thesis:
x1 in dom P1 by A25, CARD_1:47, FUNCT_2:def 1;
then A26: P1 . x1 in rng P1 by FUNCT_1:def 5;
then P1 . x1 in X1 ;
then consider P1x1 being Function of ((X \ {x}) \/ {x}),{1,0 } such that
A27: ( P1 . x1 = P1x1 & card (P1x1 " {1}) = k + 1 & P1x1 . x = 1 ) ;
X \ {x} c= (X \ {x}) \/ {x} by XBOOLE_1:7;
then A28: ( ((X \ {x}) \/ {x}) /\ (X \ {x}) = X \ {x} & dom P1x1 = (X \ {x}) \/ {x} & rng (P1x1 | (X \ {x})) c= rng P1x1 ) by FUNCT_2:def 1, RELAT_1:99, XBOOLE_1:28;
then ( dom (P1x1 | (X \ {x})) = X \ {x} & rng (P1x1 | (X \ {x})) c= {1,0 } ) by RELAT_1:90;
then reconsider Px = P1x1 | (X \ {x}) as Function of (X \ {x}),{1,0 } by FUNCT_2:4;
( not x in X \ {x} & x in {x} & dom P1x1 = (X \ {x}) \/ {x} ) by FUNCT_2:def 1, TARSKI:def 1, ZFMISC_1:64;
then ( ((X \ {x}) \/ {x}) \ {x} = X \ {x} & x in dom P1x1 ) by XBOOLE_0:def 3, ZFMISC_1:141;
then A29: P1x1 " {1} = (Px " {1}) \/ {x} by A27, A28, Th13;
not x in Px " {1} by ZFMISC_1:64;
then ( k + 1 = (card (Px " {1})) + 1 & (k + 1) - 1 = k ) by A27, A29, CARD_2:54;
then Px in Choose (X \ {x}),k,1,0 by Def1;
hence ex P1x1 being set st
( P1x1 in Choose (X \ {x}),k,1,0 & S₂[x1,P1x1] ) by A26, A27; :: thesis:

end;

consider P1x being Function of (card X1),(Choose (X \ {x}),k,1,0 ) such that
A30: for x1 being set st x1 in card X1 holds
S₂[x1,P1x . x1] from FUNCT_2:sch 1(A24);
not x in X \ {x} by ZFMISC_1:64;
then A31: card (Choose (X \ {x}),k,1,0 ) = card X1 by Th14;
for x1, x2 being set st x1 in dom P1x & x2 in dom P1x & P1x . x1 = P1x . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
assume A32: ( x1 in dom P1x & x2 in dom P1x & P1x . x1 = P1x . x2 ) ; :: thesis:
( ( Choose (X \ {x}),k,1,0 = {} implies card (Choose (X \ {x}),k,1,0 ) = {} ) & ( X1 = {} implies card X1 = {} ) ) ;
then A33: ( dom P1x = card X1 & dom P1 = card X1 ) by A31, FUNCT_2:def 1;
consider f1 being Function such that
A34: ( f1 = P1 . x1 & f1 in X1 & P1x . x1 = f1 | (X \ {x}) ) by A30, A32;
consider f2 being Function such that
A35: ( f2 = P1 . x2 & f2 in X1 & P1x . x2 = f2 | (X \ {x}) ) by A30, A32;
A36: ( ex F being Function of ((X \ {x}) \/ {x}),{1,0 } st
( f1 = F & card (F " {1}) = k + 1 & F . x = 1 ) & ex F being Function of ((X \ {x}) \/ {x}),{1,0 } st
( f2 = F & card (F " {1}) = k + 1 & F . x = 1 ) ) by A34, A35;
then A37: ( dom f1 = (X \ {x}) \/ {x} & f1 . x = 1 & dom f2 = (X \ {x}) \/ {x} & f2 . x = 1 ) by FUNCT_2:def 1;
for z being set st z in dom f1 holds
f1 . z = f2 . z

proof

let z be set ; :: thesis:
assume A38: z in dom f1 ; :: thesis:

now

per cases by A37, A38, XBOOLE_0:def 3;

suppose z in X \ {x} ; :: thesis:

then ( z in (dom f1) /\ (X \ {x}) & z in (dom f2) /\ (X \ {x}) ) by A37, A38, XBOOLE_0:def 4;
then ( (f1 | (X \ {x})) . z = f1 . z & (f2 | (X \ {x})) . z = f2 . z ) by FUNCT_1:71;
hence f1 . z = f2 . z by A32, A34, A35; :: thesis:

end;

suppose z in {x} ; :: thesis:

then z = x by TARSKI:def 1;
hence f1 . z = f2 . z by A36; :: thesis:

end;

hence f1 . z = f2 . z ; :: thesis:

end;

then ( f1 = f2 & x1 in dom P1 & x2 in dom P1 ) by A32, A33, A37, FUNCT_1:9;
hence x1 = x2 by A23, A34, A35, FUNCT_1:def 8; :: thesis:

end;

then A39: P1x is one-to-one by FUNCT_1:def 8;
set I = Intersect (Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x));
dom (Intersect (Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x))) = X \ {x} by A1, A19, Th57;
then consider XFS1 being XFinSequence of such that
A40: dom XFS1 = dom P1x and
A41: for z being set
for f being Function st z in dom XFS1 & f = P1x . z holds
XFS1 . z = card (Intersection (Intersect (Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x))),f,1) and
A42: Card_Intersection (Intersect (Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x))),k = Sum XFS1 by A31, A39, Def4;
( ( X0 = {} implies card X0 = {} ) & ( X1 = {} implies card X1 = {} ) ) ;
then A43: ( dom P0 = card X0 & dom P1 = card X1 ) by FUNCT_2:def 1;
then reconsider XP0 = P0, XP1 = P1 as XFinSequence by AFINSQ_1:7;
set Ch = Choose X,(k + 1),1,0 ;
( (X \ {x}) \/ {x} = X & not x in X \ {x} & (rng P0) \/ (rng P1) c= X0 \/ X1 ) by A1, XBOOLE_1:13, ZFMISC_1:64, ZFMISC_1:140;
then A44: ( (card X0) + (card X1) = card (Choose X,(k + 1),1,0 ) & card X0 = len XP0 & card X1 = len XP1 & rng (XP0 ^ XP1) c= X0 \/ X1 & X0 \/ X1 = Choose X,(k + 1),1,0 ) by A10, A31, A43, Lm1, Th17, AFINSQ_1:29;
then ( dom (XP0 ^ XP1) = card (Choose X,(k + 1),1,0 ) & rng (XP0 ^ XP1) c= Choose X,(k + 1),1,0 ) by AFINSQ_1:def 4;
then reconsider XP01 = XP0 ^ XP1 as Function of (card (Choose X,(k + 1),1,0 )),(Choose X,(k + 1),1,0 ) by FUNCT_2:4;
not x in X \ {x} by ZFMISC_1:64;
then X0 misses X1 by Lm1;
then rng P0 misses rng P1 by XBOOLE_1:64;
then XP01 is one-to-one by A3, A23, Th60;
then consider XFS being XFinSequence of such that
A45: dom XFS = dom XP01 and
A46: for z being set
for f being Function st z in dom XFS & f = XP01 . z holds
XFS . z = card (Intersection Fy,f,1) and
A47: Card_Intersection Fy,(k + 1) = Sum XFS by A1, Def4;
XFS = XFS0 ^ XFS1

proof

( ( Choose (X \ {x}),(k + 1),1,0 = {} implies card (Choose (X \ {x}),(k + 1),1,0 ) = {} ) & ( Choose (X \ {x}),k,1,0 = {} implies card (Choose (X \ {x}),k,1,0 ) = {} ) & ( X0 = {} implies card X0 = {} ) & ( X1 = {} implies card X1 = {} ) ) ;
then A48: ( dom P0x = card X0 & dom P0 = card X0 & dom P1x = card X1 & dom P1 = card X1 ) by A10, A31, FUNCT_2:def 1;
then ( dom (XP0 ^ XP1) = (dom XFS0) + (dom XFS1) & dom XFS0 = len XFS0 ) by A20, A40, A44, AFINSQ_1:def 4;
then A49: dom XFS = (len XFS0) + (len XFS1) by A45;
A50: for n being Element of NAT st n in dom XFS0 holds
XFS . n = XFS0 . n

proof

let n be Element of NAT ; :: thesis:
assume A51: n in dom XFS0 ; :: thesis:
consider fx being Function such that
A52: ( fx = P0 . n & fx in X0 & P0x . n = fx | (X \ {x}) ) by A9, A20, A51;
consider fx' being Function of ((X \ {x}) \/ {x}),{1,0 } such that
A53: ( fx = fx' & card (fx' " {1}) = k + 1 & fx' . x = 0 ) by A52;
( dom fx = (X \ {x}) \/ {x} & (X \ {x}) \/ {x} = X & (fx | (X \ {x})) " {1} c= dom (fx | (X \ {x})) & dom (fx | (X \ {x})) c= X \ {x} ) by A1, A53, FUNCT_2:def 1, RELAT_1:87, RELAT_1:167, ZFMISC_1:140;
then A54: ( fx " {1} = (fx | (X \ {x})) " {1} & (fx | (X \ {x})) " {1} c= X \ {x} ) by A53, Th15, XBOOLE_1:1;
consider x1 being set such that
A55: x1 in fx " {1} by A53, CARD_1:47, XBOOLE_0:def 1;
( n < dom XFS0 & (dom XFS0) + 0 <= (dom XFS0) + (dom XFS1) ) by A51, NAT_1:45, XREAL_1:9;
then ( n < (dom XFS0) + (dom XFS1) & fx . x1 in {1} ) by A55, FUNCT_1:def 13, XXREAL_0:2;
then ( n < dom XFS & XP01 . n = XP0 . n & fx . x1 = 1 & x1 in dom fx ) by A20, A40, A44, A45, A48, A51, A55, AFINSQ_1:def 4, FUNCT_1:def 13, TARSKI:def 1;
then ( n in dom XFS & XP01 . n = fx & 1 in rng fx ) by A52, FUNCT_1:def 5, NAT_1:45;
then ( XFS . n = card (Intersection Fy,fx,1) & XFS0 . n = card (Intersection (Fy | (X \ {x})),(fx | (X \ {x})),1) & Intersection (Fy | (X \ {x})),(fx | (X \ {x})),1 = Intersection (Fy | (X \ {x})),fx,1 & Intersection (Fy | (X \ {x})),fx,1 = Intersection Fy,fx,1 ) by A1, A21, A46, A51, A52, A54, Th30, Th32;
hence XFS . n = XFS0 . n ; :: thesis:

end;

for n being Element of NAT st n in dom XFS1 holds
XFS . ((len XFS0) + n) = XFS1 . n

proof

let n be Element of NAT ; :: thesis:
assume A56: n in dom XFS1 ; :: thesis:
consider fx being Function such that
A57: ( fx = P1 . n & fx in X1 & P1x . n = fx | (X \ {x}) ) by A30, A40, A56;
consider fx' being Function of ((X \ {x}) \/ {x}),{1,0 } such that
A58: ( fx = fx' & card (fx' " {1}) = k + 1 & fx' . x = 1 ) by A57;
A59: ( x in fx " {1} & dom fx = X )

proof

A60: ( dom fx' = (X \ {x}) \/ {x} & (X \ {x}) \/ {x} = X ) by A1, FUNCT_2:def 1, ZFMISC_1:140;
then ( x in dom fx & fx . x in {1} ) by A1, A58, TARSKI:def 1;
hence ( x in fx " {1} & dom fx = X ) by A58, A60, FUNCT_1:def 13; :: thesis:

end;

A61: ( 1 in rng (fx | (X \ {x})) & (fx | (X \ {x})) " {1} c= X \ {x} )

proof

A62: ( (fx | (X \ {x})) " {1} c= dom (fx | (X \ {x})) & dom (fx | (X \ {x})) = (dom fx) /\ (X \ {x}) & (dom fx) /\ (X \ {x}) c= X \ {x} ) by RELAT_1:90, RELAT_1:167, XBOOLE_1:17;
then reconsider fx1 = (fx | (X \ {x})) " {1} as finite set ;
not x in X \ {x} by ZFMISC_1:64;
then not x in (dom fx) /\ (X \ {x}) by XBOOLE_0:def 4;
then not x in dom (fx | (X \ {x})) by RELAT_1:90;
then ( {x} \/ fx1 = fx " {1} & not x in fx1 ) by A1, A58, A59, Th13, FUNCT_1:def 13;
then ( (card fx1) + 1 = k + 1 & (k + 1) - 1 = k & ((card fx1) + 1) - 1 = card fx1 ) by A58, CARD_2:54;
then consider y being set such that
A63: y in fx1 by A2, CARD_1:47, XBOOLE_0:def 1;
( y in dom (fx | (X \ {x})) & (fx | (X \ {x})) . y in {1} ) by A63, FUNCT_1:def 13;
then ( (fx | (X \ {x})) . y in rng (fx | (X \ {x})) & (fx | (X \ {x})) . y = 1 ) by FUNCT_1:def 5, TARSKI:def 1;
hence ( 1 in rng (fx | (X \ {x})) & (fx | (X \ {x})) " {1} c= X \ {x} ) by A62, XBOOLE_1:1; :: thesis:

end;

( n < dom XFS1 & n in dom XP1 ) by A40, A48, A56, NAT_1:45;
then ( (dom XFS0) + n < (dom XFS0) + (dom XFS1) & n in dom XP1 ) by XREAL_1:10;
then ( (dom XFS0) + n < dom XFS & XP1 . n = XP01 . (n + (len XP0)) & dom XFS0 = dom XP0 ) by A20, A40, A44, A45, A48, AFINSQ_1:def 4;
then ( (dom XFS0) + n in dom XFS & XP01 . (n + (len XP0)) = fx & len XP0 = dom XFS0 ) by A57, NAT_1:45;
then ( XFS . ((dom XFS0) + n) = card (Intersection Fy,fx,1) & XFS1 . n = card (Intersection (Intersect (Fy | (X \ {x})),((X \ {x}) --> (Fy . x))),(fx | (X \ {x})),1) & Intersection (Intersect (Fy | (X \ {x})),((X \ {x}) --> (Fy . x))),(fx | (X \ {x})),1 = (Intersection (Fy | (X \ {x})),(fx | (X \ {x})),1) /\ (Fy . x) & Intersection (Fy | (X \ {x})),(fx | (X \ {x})),1 = Intersection Fy,(fx | (X \ {x})),1 ) by A1, A19, A41, A46, A56, A57, A61, Th32, Th59;
then ( XFS . ((dom XFS0) + n) = card (Intersection Fy,fx,1) & XFS1 . n = card ((Intersection Fy,(fx | (X \ {x})),1) /\ (Fy . x)) & (Intersection Fy,(fx | (X \ {x})),1) /\ (Fy . x) = Intersection Fy,fx,1 ) by A59, Th34;
hence XFS . ((len XFS0) + n) = XFS1 . n ; :: thesis:

end;

hence XFS = XFS0 ^ XFS1 by A49, A50, AFINSQ_1:def 4; :: thesis:

end;

then ( addnat "**" XFS = addnat . (addnat "**" XFS0),(addnat "**" XFS1) & addnat "**" XFS0 = Card_Intersection (Fy | ((dom Fy) \ {x})),(k + 1) & addnat "**" XFS1 = Card_Intersection (Intersect (Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x))),k & addnat "**" XFS = Card_Intersection Fy,(k + 1) ) by A22, A42, A47, STIRL2_1:47, STIRL2_1:def 4;
hence Card_Intersection Fy,(k + 1) = (Card_Intersection (Fy | ((dom Fy) \ {x})),(k + 1)) + (Card_Intersection (Intersect (Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x))),k) by BINOP_2:def 23; :: thesis: