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 ) by XBOOLE_1:2;
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, CARD_1:47; :: thesis: Card_Intersection Fy,1 = Sum XFS
Sum XFS = 0 ;
hence Card_Intersection Fy,1 = Sum XFS by A1, A3, Th51, CARD_1:47; :: 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:7;
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( set ) -> set = ((P . $1) .--> 0 ) +* ((X \ {(P . $1)}) --> 1);
A6: for x being set st x in cX holds
H2(x) in Choose X,1,0 ,1
proof
let x be set ; :: 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:47, FUNCT_2:def 1;
then P . x in rng P by FUNCT_1:def 5;
then A7: {(P . x)} \/ (X \ {(P . x)}) = X by ZFMISC_1:140;
( {(P . x)} misses X \ {(P . x)} & card {(P . x)} = 1 ) by CARD_1:50, XBOOLE_1:79;
hence H2(x) in Choose X,1,0 ,1 by A7, Th20; :: thesis: verum
end;
consider P1 being Function of cX,(Choose X,1,0 ,1) such that
A8: for z being set 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, STIRL2_1:70;
let z be set ; :: 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 set such that
A12: F " {0 } = {x1} by A11, CARD_2:60;
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 set such that
A14: x2 in dom P and
A15: P . x2 = x1 by FUNCT_1:def 5;
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:140;
A18: now
let d be set ; :: 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
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)} ) by FUNCOP_1:19;
then (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = ((P . x2) .--> 0 ) . d by A20, A21, FUNCT_4:17;
then A22: (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = 0 by A20, FUNCOP_1:13;
F . d in {0 } by A12, A15, A20, FUNCT_1:def 13;
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) by FUNCT_2:def 1;
then (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = ((X \ {(P . x2)}) --> 1) . d by FUNCT_4:14;
then A24: (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = 1 by A23, FUNCOP_1:13;
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 13;
then A26: not F . d = 0 by TARSKI:def 1;
F . d in rng F by A23, A25, FUNCT_1:def 5;
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;
dom ((P . x2) .--> 0 ) = {(P . x2)} by FUNCOP_1:19;
then A27: X = (dom ((P . x2) .--> 0 )) \/ (dom ((X \ {(P . x2)}) --> 1)) by A17, FUNCT_2:def 1;
( 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, FUNCT_1:9;
hence P1 . x2 = F by A8, A14; :: thesis: verum
end;
card (Choose X,1,0 ,1) = (card X) choose 1 by Th18;
then card (Choose X,1,0 ,1) = cX by NAT_1:14, NEWTON:33;
then dom P1 = cX by CARD_1:47, FUNCT_2:def 1;
hence z in rng P1 by A10, A14, A16, FUNCT_1:def 5; :: thesis: verum
end;
then A28: Choose X,1,0 ,1 = rng P1 by XBOOLE_0:def 10;
then A29: P1 is onto by FUNCT_2:def 3;
card (Choose X,1,0 ,1) = (card X) choose 1 by Th18;
then A30: card X = card (Choose X,1,0 ,1) by A28, NAT_1:14, NEWTON:33;
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, STIRL2_1:70;
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, Def4;
( 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 set st z in dom XFS1 holds
XFS1 . z = XFS . z
proof
let z be set ; :: 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 set such that
A39: f " {0 } = {x1} by A38, CARD_2:60;
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;
A42: dom ((X \ {(P . z)}) --> 1) = X \ {(P . z)} by FUNCOP_1:19;
A43: P . z in {(P . z)} by TARSKI:def 1;
{(P . z)} = dom ((P . z) .--> 0 ) by FUNCOP_1:19;
then 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, FUNCOP_1:13, XBOOLE_0:def 5;
then A45: H2(z) . (P . z) = 0 by A44, A42, 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 13;
then P . z = x1 by A39, TARSKI:def 1;
then A47: card (Intersection Fy,f,0 ) = card (Fy . (P . z)) by A39, Th37;
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:23; :: 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 17; :: thesis: verum
end;
end;
end;