let x, y be set ; :: thesis: for X, Y being finite set
for Fy being finite-yielding Function st x <> y & Fy = x,y --> X,Y holds
( Card_Intersection Fy,1 = (card X) + (card Y) & Card_Intersection Fy,2 = card (X /\ Y) )
let X, Y be finite set ; :: thesis: for Fy being finite-yielding Function st x <> y & Fy = x,y --> X,Y holds
( Card_Intersection Fy,1 = (card X) + (card Y) & Card_Intersection Fy,2 = card (X /\ Y) )
let Fy be finite-yielding Function; :: thesis: ( x <> y & Fy = x,y --> X,Y implies ( Card_Intersection Fy,1 = (card X) + (card Y) & Card_Intersection Fy,2 = card (X /\ Y) ) )
assume A1: ( x <> y & Fy = x,y --> X,Y ) ; :: thesis: ( Card_Intersection Fy,1 = (card X) + (card Y) & Card_Intersection Fy,2 = card (X /\ Y) )
set P = 0 ,1 --> x,y;
( dom (0 ,1 --> x,y) = {0 ,1} & rng (0 ,1 --> x,y) = {x,y} & card {x,y} = 2 & 2 = {0 ,1} ) by A1, CARD_1:88, CARD_2:76, FUNCT_4:65, FUNCT_4:67;
then reconsider P = 0 ,1 --> x,y as Function of (card {x,y}),{x,y} by FUNCT_2:3;
rng P = {x,y} by FUNCT_4:67;
then ( P is onto & card (card {x,y}) = card {x,y} ) by FUNCT_2:def 3;
then ( P is one-to-one & dom Fy = {x,y} ) by A1, FUNCT_4:65, STIRL2_1:70;
then consider XFS being XFinSequence of such that
A2: dom XFS = card {x,y} and
A3: for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) and
A4: Card_Intersection Fy,1 = Sum XFS by Th52;
dom P = {0 ,1} by FUNCT_4:65;
then ( dom XFS = 2 & 2 = {0 ,1} & 0 in dom P & 1 in dom P ) by A1, A2, CARD_1:88, CARD_2:76, TARSKI:def 2;
then ( len XFS = 2 & 0 in dom XFS & 1 in dom XFS & P . 0 = x & P . 1 = y & Fy . x = X & Fy . y = Y & (Fy * P) . 0 = Fy . (P . 0 ) & (Fy * P) . 1 = Fy . (P . 1) ) by A1, FUNCT_1:23, FUNCT_4:66, TARSKI:def 2;
then ( XFS = <%(XFS . 0 ),(XFS . 1)%> & XFS . 0 = card X & XFS . 1 = card Y ) by A3, AFINSQ_1:42;
then addnat "**" XFS = addnat . (card X),(card Y) by STIRL2_1:48;
then A5: addnat "**" XFS = (card X) + (card Y) by BINOP_2:def 23;
0 in {0 } by TARSKI:def 1;
then ( ({x,y} --> 0 ) " {0 } = {x,y} & card {x,y} = 2 & dom Fy = {x,y} & Fy . x = X & Fy . y = Y ) by A1, CARD_2:76, FUNCOP_1:20, FUNCT_4:65, FUNCT_4:66;
then ( Intersection Fy,({x,y} --> 0 ),0 = X /\ Y & Card_Intersection Fy,2 = card (Intersection Fy,({x,y} --> 0 ),0 ) ) by Th38, Th53;
hence ( Card_Intersection Fy,1 = (card X) + (card Y) & Card_Intersection Fy,2 = card (X /\ Y) ) by A4, A5, STIRL2_1:def 4; :: thesis: verum