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;
card X > 0 by A2;
then reconsider k = (card X) - 1 as Element of NAT by NAT_1:20;
set Xx = X \ {x};
A3: ( X \ {x} = {} implies card (X \ {x}) = {} ) ;
consider Px being Function of (card (X \ {x})),(X \ {x}) such that
A4: Px is one-to-one by Lm2;
not card (X \ {x}) in card (X \ {x}) ;
then consider P being Function of ((card (X \ {x})) \/ {(card (X \ {x}))}),((X \ {x}) \/ {x}) such that
A5: P | (card (X \ {x})) = Px and
A6: P . (card (X \ {x})) = x by A3, STIRL2_1:57;
not x in X \ {x} by ZFMISC_1:56;
then A7: P is one-to-one by A4, A3, A5, A6, STIRL2_1:58;
A8: card X = Segm (k + 1) ;
then A9: card (X \ {x}) = Segm k by A2, STIRL2_1:55;
then card X = (card (X \ {x})) \/ {(card (X \ {x}))} by A8, AFINSQ_1:2;
then reconsider P = P as Function of (card X),X by A2, ZFMISC_1:116;
consider XFS being XFinSequence of NAT such that
A10: dom XFS = card X and
A11: for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) and
A12: Card_Intersection (Fy,1) = Sum XFS by A7, Th43;
A13: P . k = x by A2, A6, A8, STIRL2_1:55;
X /\ (X \ {x}) = X \ {x} by XBOOLE_1:28;
then dom (Fy | (X \ {x})) = X \ {x} by RELAT_1:61;
then consider XFSx being XFinSequence of NAT such that
A14: dom XFSx = card (X \ {x}) and
A15: for z being set st z in dom XFSx holds
XFSx . z = card (((Fy | (X \ {x})) * Px) . z) and
A16: Card_Intersection ((Fy | (X \ {x})),1) = Sum XFSx by A4, Th43;
k < k + 1 by NAT_1:13;
then A17: Segm k c= Segm (k + 1) by NAT_1:39;
A18: for y being object st y in dom XFSx holds
XFS . y = XFSx . y

proof

A19: ( X \ {x} = X /\ (X \ {x}) & X /\ (X \ {x}) = dom (Fy | (X \ {x})) ) by RELAT_1:61, XBOOLE_1:28;
let y be object ; :: thesis: ( y in dom XFSx implies XFS . y = XFSx . y )
assume A20: y in dom XFSx ; :: thesis: XFS . y = XFSx . y
A21: XFS . y = card ((Fy * P) . y) by A14, A9, A10, A11, A17, A20;
A22: dom Px = k by A3, A9, FUNCT_2:def 1;
then Px . y in rng Px by A14, A9, A20, FUNCT_1:def 3;
then A23: (Fy | (X \ {x})) . (Px . y) = Fy . (Px . y) by A19, FUNCT_1:47;
dom P = k + 1 by CARD_1:27, FUNCT_2:def 1;
then A24: (Fy * P) . y = Fy . (P . y) by A14, A9, A17, A20, FUNCT_1:13;
Px . y = P . y by A14, A5, A9, A20, A22, FUNCT_1:47;
then (Fy * P) . y = ((Fy | (X \ {x})) * Px) . y by A14, A9, A20, A22, A24, A23, FUNCT_1:13;
hence XFS . y = XFSx . y by A15, A20, A21; :: thesis: verum

end;

k < k + 1 by NAT_1:13;
then A25: k in Segm (k + 1) by NAT_1:44;
then k in dom P by CARD_1:27, FUNCT_2:def 1;
then A26: (Fy * P) . k = Fy . (P . k) by FUNCT_1:13;
(dom XFS) /\ k = dom XFSx by A14, A9, A10, A17, XBOOLE_1:28;
then XFS | k = XFSx by A18, FUNCT_1:46;
then A27: (Sum XFSx) + (XFS . k) = Sum (XFS | (k + 1)) by A10, A25, AFINSQ_2:65;
XFS . k = card ((Fy * P) . k) by A10, A11, A25;
hence Card_Intersection (Fy,1) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),1)) + (card (Fy . x)) by A16, A10, A12, A27, A26, A13; :: thesis: verum