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:62, FUNCT_4:64;
card {x,y} = 2
by A1, CARD_2:57;
then reconsider P = (0,1) --> (x,y) as Function of (card {x,y}),{x,y} by A3, CARD_1:50, FUNCT_2:1;
A4:
card (card {x,y}) = card {x,y}
;
A5:
( P . 0 = x & Fy . x = X )
by A1, A2, FUNCT_4:63;
A6:
( P . 1 = y & Fy . y = Y )
by A2, FUNCT_4:63;
A7:
dom Fy = {x,y}
by A2, FUNCT_4:62;
rng P = {x,y}
by FUNCT_4:64;
then
P is onto
by FUNCT_2:def 3;
then
P is one-to-one
by A4, FINSEQ_4:63;
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, Th43;
len XFS = 2
by A1, A8, CARD_2:57;
then A11:
XFS = <%(XFS . 0),(XFS . 1)%>
by AFINSQ_1:38;
A12:
dom P = {0,1}
by FUNCT_4:62;
then
1 in dom P
by TARSKI:def 2;
then A13:
(Fy * P) . 1 = Fy . (P . 1)
by FUNCT_1:13;
0 in {0}
by TARSKI:def 1;
then A14:
({x,y} --> 0) " {0} = {x,y}
by FUNCOP_1:14;
( Fy . x = X & Fy . y = Y )
by A1, A2, FUNCT_4:63;
then A15:
Intersection (Fy,({x,y} --> 0),0) = X /\ Y
by A14, Th35;
0 in dom P
by A12, TARSKI:def 2;
then A16:
(Fy * P) . 0 = Fy . (P . 0)
by FUNCT_1:13;
A17:
dom XFS = 2
by A1, A8, CARD_2:57;
then
1 in dom XFS
by CARD_1:50, TARSKI:def 2;
then A18:
XFS . 1 = card Y
by A9, A6, A13;
0 in dom XFS
by A17, CARD_1:50, 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:38;
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:57, FUNCT_4:62;
hence
( Card_Intersection (Fy,1) = (card X) + (card Y) & Card_Intersection (Fy,2) = card (X /\ Y) )
by A10, A19, A15, Th44, AFINSQ_2:51; verum