let Fy be finite-yielding Function; :: thesis: for X being finite set st dom Fy = X holds
for P being Function of (card X),X st P is one-to-one holds
ex XFS being XFinSequence of NAT st
( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )
let X be finite set ; :: thesis: ( dom Fy = X implies for P being Function of (card X),X st P is one-to-one holds
ex XFS being XFinSequence of NAT st
( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS ) )
assume A1: dom Fy = X ; :: thesis: for P being Function of (card X),X st P is one-to-one holds
ex XFS being XFinSequence of NAT st
( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )
let P be Function of (card X),X; :: thesis: ( P is one-to-one implies ex XFS being XFinSequence of NAT st
( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS ) )
assume A2: P is one-to-one ; :: thesis: ex XFS being XFinSequence of NAT st
( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )
per cases ( X = {} or X <> {} ) ;
suppose A3: X = {} ; :: thesis: ex XFS being XFinSequence of NAT st
( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )
reconsider XFS = {} as XFinSequence ;
( rng {} c= {} & {} c= NAT ) ;
then reconsider XFS = XFS as XFinSequence of NAT by RELAT_1:def 19;
take XFS ; :: thesis: ( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )
thus ( card X = dom XFS & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) ) by A3; :: thesis: Card_Intersection (Fy,1) = Sum XFS
Sum XFS = 0 ;
hence Card_Intersection (Fy,1) = Sum XFS by A1, A3, Th42, CARD_1:27; :: thesis: verum
end;
suppose X <> {} ; :: thesis: ex XFS being XFinSequence of NAT st
( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )
then reconsider cX = card X as non empty set ;
deffunc H1( Element of cX) -> Element of NAT = card ((Fy * P) . $1);
consider XFS being Function of cX,NAT such that
A4: for x being Element of cX holds XFS . x = H1(x) from FUNCT_2:sch 4();
A5: dom XFS = cX by FUNCT_2:def 1;
then reconsider XFS = XFS as XFinSequence by AFINSQ_1:5;
reconsider XFS = XFS as XFinSequence of NAT ;
take XFS ; :: thesis: ( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )
thus card X = dom XFS by FUNCT_2:def 1; :: thesis: ( ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )
thus for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) by A4, A5; :: thesis: Card_Intersection (Fy,1) = Sum XFS
thus Card_Intersection (Fy,1) = Sum XFS :: thesis: verum
proof
deffunc H2( object ) -> set = ((P . $1) .--> 0) +* ((X \ {(P . $1)}) --> 1);
A6: for x being object st x in cX holds
H2(x) in Choose (X,1,0,1)
proof
let x be object ; :: thesis: ( x in cX implies H2(x) in Choose (X,1,0,1) )
assume x in cX ; :: thesis: H2(x) in Choose (X,1,0,1)
then x in dom P by CARD_1:27, FUNCT_2:def 1;
then P . x in rng P by FUNCT_1:def 3;
then A7: {(P . x)} \/ (X \ {(P . x)}) = X by ZFMISC_1:116;
( {(P . x)} misses X \ {(P . x)} & card {(P . x)} = 1 ) by CARD_1:30, XBOOLE_1:79;
hence H2(x) in Choose (X,1,0,1) by A7, Th17; :: thesis: verum
end;
consider P1 being Function of cX,(Choose (X,1,0,1)) such that
A8: for z being object st z in cX holds
P1 . z = H2(z) from FUNCT_2:sch 2(A6);
 Choose (X,1,0,1) c= rng P1
proof
card X = card (card X) ;
then A9: P is onto by A2, FINSEQ_4:63;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose (X,1,0,1) or z in rng P1 )
assume z in Choose (X,1,0,1) ; :: thesis: z in rng P1
then consider F being Function of X,{0,1} such that
A10: F = z and
A11: card (F " {0}) = 1 by Def1;
consider x1 being object such that
A12: F " {0} = {x1} by A11, CARD_2:42;
A13: x1 in {x1} by TARSKI:def 1;
then x1 in X by A12;
then x1 in rng P by A9, FUNCT_2:def 3;
then consider x2 being object such that
A14: x2 in dom P and
A15: P . x2 = x1 by FUNCT_1:def 3;
A16: P1 . x2 = F
proof
set F1 = (X \ {(P . x2)}) --> 1;
set F0 = (P . x2) .--> 0;
set P1x = ((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1);
A17: {(P . x2)} \/ (X \ {(P . x2)}) = X by A12, A13, A15, ZFMISC_1:116;
A18: now :: thesis: for d being object st d in dom F holds
(((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = F . d
let d be object ; :: thesis: ( d in dom F implies (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = F . d )
assume A19: d in dom F ; :: thesis: (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = F . d
now :: thesis: (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = F . d
per cases ( d in {(P . x2)} or d in X \ {(P . x2)} ) by A17, A19, XBOOLE_0:def 3;
suppose A20: d in {(P . x2)} ; :: thesis: (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = F . d
A21: {(P . x2)} misses X \ {(P . x2)} by XBOOLE_1:79;
( dom ((P . x2) .--> 0) = {(P . x2)} & dom ((X \ {(P . x2)}) --> 1) = X \ {(P . x2)} ) ;
then (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = ((P . x2) .--> 0) . d by A20, A21, FUNCT_4:16;
then A22: (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = 0 ;
F . d in {0} by A12, A15, A20, FUNCT_1:def 7;
hence (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = F . d by A22, TARSKI:def 1; :: thesis: verum
end;
suppose A23: d in X \ {(P . x2)} ; :: thesis: (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = F . d
then d in dom ((X \ {(P . x2)}) --> 1) ;
then (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = ((X \ {(P . x2)}) --> 1) . d by FUNCT_4:13;
then A24: (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = 1 by A23, FUNCOP_1:7;
A25: X = dom F by FUNCT_2:def 1;
not d in {x1} by A15, A23, XBOOLE_0:def 5;
then not F . d in {0} by A12, A23, A25, FUNCT_1:def 7;
then A26: not F . d = 0 by TARSKI:def 1;
F . d in rng F by A23, A25, FUNCT_1:def 3;
hence (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = F . d by A24, A26, TARSKI:def 2; :: thesis: verum
end;
end;
end;
hence (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) . d = F . d ; :: thesis: verum
end;
A27: X = (dom ((P . x2) .--> 0)) \/ (dom ((X \ {(P . x2)}) --> 1)) by A17;
( dom F = X & dom (((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1)) = (dom ((P . x2) .--> 0)) \/ (dom ((X \ {(P . x2)}) --> 1)) ) by FUNCT_2:def 1, FUNCT_4:def 1;
then ((P . x2) .--> 0) +* ((X \ {(P . x2)}) --> 1) = F by A27, A18;
hence P1 . x2 = F by A8, A14; :: thesis: verum
end;
card (Choose (X,1,0,1)) = (card X) choose 1 by Th15;
then card (Choose (X,1,0,1)) = cX by NAT_1:14, NEWTON:23;
then dom P1 = cX by CARD_1:27, FUNCT_2:def 1;
hence z in rng P1 by A10, A14, A16, FUNCT_1:def 3; :: thesis: verum
end;
then A28: Choose (X,1,0,1) = rng P1 ;
then A29: P1 is onto by FUNCT_2:def 3;
card (Choose (X,1,0,1)) = (card X) choose 1 by Th15;
then A30: card X = card (Choose (X,1,0,1)) by A28, NAT_1:14, NEWTON:23;
then reconsider P1 = P1 as Function of (card (Choose (X,1,0,1))),(Choose (X,1,0,1)) ;
card (card X) = card X ;
then P1 is one-to-one by A29, A30, FINSEQ_4:63;
then consider XFS1 being XFinSequence of NAT such that
A31: dom XFS1 = dom P1 and
A32: for z being set
for f being Function st z in dom XFS1 & f = P1 . z holds
XFS1 . z = card (Intersection (Fy,f,0)) and
A33: Card_Intersection (Fy,1) = Sum XFS1 by A1, Def3;
( Choose (X,1,0,1) = {} implies card (Choose (X,1,0,1)) = {} ) ;
then A34: dom P1 = card (Choose (X,1,0,1)) by FUNCT_2:def 1;
A35: for z being object st z in dom XFS1 holds
XFS1 . z = XFS . z
proof
let z be object ; :: thesis: ( z in dom XFS1 implies XFS1 . z = XFS . z )
assume A36: z in dom XFS1 ; :: thesis: XFS1 . z = XFS . z
H2(z) in Choose (X,1,0,1) by A6, A30, A31, A36;
then consider f being Function of X,{0,1} such that
A37: f = H2(z) and
A38: card (f " {0}) = 1 by Def1;
consider x1 being object such that
A39: f " {0} = {x1} by A38, CARD_2:42;
P1 . z = H2(z) by A8, A30, A31, A36;
then A40: XFS1 . z = card (Intersection (Fy,f,0)) by A32, A36, A37;
A41: 0 in {0} by TARSKI:def 1;
A43: P . z in {(P . z)} by TARSKI:def 1;
A44: P . z in (dom ((P . z) .--> 0)) \/ (dom ((X \ {(P . z)}) --> 1)) by A43, XBOOLE_0:def 3;
( not P . z in X \ {(P . z)} & ((P . z) .--> 0) . (P . z) = 0 ) by A43, XBOOLE_0:def 5;
then A45: H2(z) . (P . z) = 0 by A44, FUNCT_4:def 1;
P . z in dom H2(z) by A44, FUNCT_4:def 1;
then A46: P . z in f " {0} by A37, A45, A41, FUNCT_1:def 7;
then P . z = x1 by A39, TARSKI:def 1;
then A47: card (Intersection (Fy,f,0)) = card (Fy . (P . z)) by A39, Th34;
A48: XFS . z = card ((Fy * P) . z) by A4, A30, A31, A36;
z in dom P by A30, A31, A34, A36, A46, FUNCT_2:def 1;
hence XFS1 . z = XFS . z by A47, A40, A48, FUNCT_1:13; :: thesis: verum
end;
dom XFS1 = dom XFS by A30, A31, A34, FUNCT_2:def 1;
hence Card_Intersection (Fy,1) = Sum XFS by A33, A35, FUNCT_1:def 11; :: thesis: verum
end;
end;
end;