let Fy be finite-yielding Function; :: thesis: for x being set st dom Fy is finite & x in dom Fy holds
Card_Intersection Fy,1 = (Card_Intersection (Fy | ((dom Fy) \ {x})),1) + (card (Fy . x))
let x be set ; :: thesis: ( dom Fy is finite & x in dom Fy implies Card_Intersection Fy,1 = (Card_Intersection (Fy | ((dom Fy) \ {x})),1) + (card (Fy . x)) )
assume that
A1: dom Fy is finite and
A2: x in dom Fy ; :: thesis: Card_Intersection Fy,1 = (Card_Intersection (Fy | ((dom Fy) \ {x})),1) + (card (Fy . x))
reconsider X = dom Fy as finite set by A1;
set Xx = X \ {x};
consider Px being Function of (card (X \ {x})),(X \ {x}) such that
A3: Px is one-to-one by Lm3;
X /\ (X \ {x}) = X \ {x} by XBOOLE_1:28;
then dom (Fy | (X \ {x})) = X \ {x} by RELAT_1:90;
then consider XFSx being XFinSequence of such that
A4: dom XFSx = card (X \ {x}) and
A5: for z being set st z in dom XFSx holds
XFSx . z = card (((Fy | (X \ {x})) * Px) . z) and
A6: Card_Intersection (Fy | (X \ {x})),1 = Sum XFSx by A3, Th52;
card X <> 0 by A2;
then card X > 0 ;
then reconsider k = (card X) - 1 as Element of NAT by NAT_1:20;
A7: ( not card (X \ {x}) in card (X \ {x}) & ( X \ {x} = {} implies card (X \ {x}) = {} ) ) ;
then consider P being Function of ((card (X \ {x})) \/ {(card (X \ {x}))}),((X \ {x}) \/ {x}) such that
A8: ( P | (card (X \ {x})) = Px & P . (card (X \ {x})) = x ) by STIRL2_1:67;
not x in X \ {x} by ZFMISC_1:64;
then A9: P is one-to-one by A3, A7, A8, STIRL2_1:68;
A10: card X = k + 1 ;
then A11: card (X \ {x}) = k by A2, STIRL2_1:65;
then ( card X = (card (X \ {x})) \/ {(card (X \ {x}))} & (X \ {x}) \/ {x} = X ) by A2, A10, AFINSQ_1:4, ZFMISC_1:140;
then reconsider P = P as Function of (card X),X ;
consider XFS being XFinSequence of such that
A12: dom XFS = card X and
A13: for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) and
A14: Card_Intersection Fy,1 = Sum XFS by A9, Th52;
A15: XFS | k = XFSx

proof

k < k + 1 by NAT_1:13;
then A16: k c= k + 1 by NAT_1:40;
then A17: (dom XFS) /\ k = dom XFSx by A4, A11, A12, XBOOLE_1:28;
for y being set st y in dom XFSx holds
XFS . y = XFSx . y

proof

let y be set ; :: thesis: ( y in dom XFSx implies XFS . y = XFSx . y )
assume A18: y in dom XFSx ; :: thesis: XFS . y = XFSx . y
A19: ( dom Px = k & dom P = k + 1 ) by A7, A11, CARD_1:47, FUNCT_2:def 1;
then A20: ( Px . y = P . y & (Fy * P) . y = Fy . (P . y) & y in dom XFS ) by A4, A8, A11, A12, A16, A18, FUNCT_1:23, FUNCT_1:70;
( Px . y in rng Px & X \ {x} c= X ) by A4, A11, A18, A19, FUNCT_1:def 5;
then ( Px . y in X \ {x} & X \ {x} = X /\ (X \ {x}) & X /\ (X \ {x}) = dom (Fy | (X \ {x})) ) by RELAT_1:90, XBOOLE_1:28;
then ( ((Fy | (X \ {x})) * Px) . y = (Fy | (X \ {x})) . (Px . y) & (Fy | (X \ {x})) . (Px . y) = Fy . (Px . y) ) by A4, A11, A18, A19, FUNCT_1:23, FUNCT_1:70;
then ( (Fy * P) . y = ((Fy | (X \ {x})) * Px) . y & XFS . y = card ((Fy * P) . y) ) by A13, A20;
hence XFS . y = XFSx . y by A5, A18; :: thesis: verum

end;

hence XFS | k = XFSx by A17, FUNCT_1:68; :: thesis: verum

end;

k < k + 1 by NAT_1:13;
then A21: k in card X by NAT_1:45;
then A22: ( (Sum XFSx) + (XFS . k) = Sum (XFS | (k + 1)) & XFS . k = card ((Fy * P) . k) ) by A12, A13, A15, Th44;
k in dom P by A21, CARD_1:47, FUNCT_2:def 1;
then ( (Fy * P) . k = Fy . (P . k) & P . k = x & XFS | (k + 1) = XFS ) by A2, A8, A10, A12, FUNCT_1:23, RELAT_1:98, STIRL2_1:65;
hence Card_Intersection Fy,1 = (Card_Intersection (Fy | ((dom Fy) \ {x})),1) + (card (Fy . x)) by A6, A14, A22; :: thesis: verum