let x, y be set ; 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 ; 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; ( x <> y & Fy = x,y --> X,Y implies ( Card_Intersection Fy,1 = (card X) + (card Y) & Card_Intersection Fy,2 = card (X /\ Y) ) )
assume that
A1:
x <> y
and
A2:
Fy = x,y --> X,Y
; ( Card_Intersection Fy,1 = (card X) + (card Y) & Card_Intersection Fy,2 = card (X /\ Y) )
set P = 0 ,1 --> x,y;
A3:
( dom (0 ,1 --> x,y) = {0 ,1} & rng (0 ,1 --> x,y) = {x,y} )
by FUNCT_4:65, FUNCT_4:67;
card {x,y} = 2
by A1, CARD_2:76;
then reconsider P = 0 ,1 --> x,y as Function of (card {x,y}),{x,y} by A3, CARD_1:88, FUNCT_2:3;
A4:
card (card {x,y}) = card {x,y}
;
A5:
( P . 0 = x & Fy . x = X )
by A1, A2, FUNCT_4:66;
A6:
( P . 1 = y & Fy . y = Y )
by A2, FUNCT_4:66;
A7:
dom Fy = {x,y}
by A2, FUNCT_4:65;
rng P = {x,y}
by FUNCT_4:67;
then
P is onto
by FUNCT_2:def 3;
then
P is one-to-one
by A4, STIRL2_1:70;
then consider XFS being XFinSequence of NAT such that
A8:
dom XFS = card {x,y}
and
A9:
for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z)
and
A10:
Card_Intersection Fy,1 = Sum XFS
by A7, Th52;
len XFS = 2
by A1, A8, CARD_2:76;
then A11:
XFS = <%(XFS . 0 ),(XFS . 1)%>
by AFINSQ_1:42;
A12:
dom P = {0 ,1}
by FUNCT_4:65;
then
1 in dom P
by TARSKI:def 2;
then A13:
(Fy * P) . 1 = Fy . (P . 1)
by FUNCT_1:23;
0 in {0 }
by TARSKI:def 1;
then A14:
({x,y} --> 0 ) " {0 } = {x,y}
by FUNCOP_1:20;
( Fy . x = X & Fy . y = Y )
by A1, A2, FUNCT_4:66;
then A15:
Intersection Fy,({x,y} --> 0 ),0 = X /\ Y
by A14, Th38;
0 in dom P
by A12, TARSKI:def 2;
then A16:
(Fy * P) . 0 = Fy . (P . 0 )
by FUNCT_1:23;
A17:
dom XFS = 2
by A1, A8, CARD_2:76;
then
1 in dom XFS
by CARD_1:88, TARSKI:def 2;
then A18:
XFS . 1 = card Y
by A9, A6, A13;
0 in dom XFS
by A17, CARD_1:88, TARSKI:def 2;
then
XFS . 0 = card X
by A9, A5, A16;
then
addnat "**" XFS = addnat . (card X),(card Y)
by A11, A18, AFINSQ_2:50;
then A19:
addnat "**" XFS = (card X) + (card Y)
by BINOP_2:def 23;
( card {x,y} = 2 & dom Fy = {x,y} )
by A1, A2, CARD_2:76, FUNCT_4:65;
hence
( Card_Intersection Fy,1 = (card X) + (card Y) & Card_Intersection Fy,2 = card (X /\ Y) )
by A10, A19, A15, Th53, AFINSQ_2:63; verum