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 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 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 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 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 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 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 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 & Card_Intersection Fy,1 = 0 ) by A1, A3, Th51, CARD_1:47, STIRL2_1:53;
hence Card_Intersection Fy,1 = Sum XFS ; :: thesis: verum
end;
suppose X <> {} ; :: thesis: ex XFS being XFinSequence of 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 & rng XFS c= NAT ) by FUNCT_2:def 1;
then reconsider XFS = XFS as XFinSequence by AFINSQ_1:7;
reconsider XFS = XFS as XFinSequence of ;
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 A7: x in cX ; :: thesis: H2(x) in Choose X,1,0 ,1
x in dom P by A7, CARD_1:47, FUNCT_2:def 1;
then P . x in rng P by FUNCT_1:def 5;
then ( {(P . x)} \/ (X \ {(P . x)}) = X & {(P . x)} misses X \ {(P . x)} & card {(P . x)} = 1 ) by CARD_1:50, XBOOLE_1:79, ZFMISC_1:140;
hence H2(x) in Choose X,1,0 ,1 by 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
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose X,1,0 ,1 or z in rng P1 )
assume A9: z in Choose X,1,0 ,1 ; :: thesis: z in rng P1
consider F being Function of X,{0 ,1} such that
A10: ( F = z & card (F " {0 }) = 1 ) by A9, Def1;
consider x1 being set such that
A11: F " {0 } = {x1} by A10, CARD_2:60;
A12: x1 in {x1} by TARSKI:def 1;
then ( x1 in dom F & dom F = X & card X = card (card X) ) by A11, FUNCT_1:def 13, FUNCT_2:def 1;
then ( x1 in X & P is onto ) by A2, STIRL2_1:70;
then x1 in rng P by FUNCT_2:def 3;
then consider x2 being set such that
A13: ( x2 in dom P & P . x2 = x1 ) by FUNCT_1:def 5;
cX <> 0 ;
then ( card (Choose X,1,0 ,1) = (card X) choose 1 & card X >= 1 ) by Th18, NAT_1:14;
then card (Choose X,1,0 ,1) = cX by NEWTON:33;
then A14: ( dom P = cX & dom P1 = cX ) by CARD_1:47, FUNCT_2:def 1;
P1 . x2 = F
proof
set F0 = (P . x2) .--> 0 ;
set F1 = (X \ {(P . x2)}) --> 1;
set P1x = ((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1);
A15: ( {(P . x2)} \/ (X \ {(P . x2)}) = X & dom ((P . x2) .--> 0 ) = {(P . x2)} ) by A11, A12, A13, FUNCOP_1:19, ZFMISC_1:140;
then A16: ( dom F = X & X = (dom ((P . x2) .--> 0 )) \/ (dom ((X \ {(P . x2)}) --> 1)) & 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;
now
let d be set ; :: thesis: ( d in dom F implies (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = F . d )
assume A17: 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 A15, A17, XBOOLE_0:def 3;
suppose A18: d in {(P . x2)} ; :: thesis: (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = F . d
then ( d = P . x2 & dom ((P . x2) .--> 0 ) = {(P . x2)} & dom ((X \ {(P . x2)}) --> 1) = X \ {(P . x2)} & {(P . x2)} misses X \ {(P . x2)} ) by FUNCOP_1:19, TARSKI:def 1, XBOOLE_1:79;
then ( (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = ((P . x2) .--> 0 ) . d & d in F " {0 } ) by A11, A13, A18, FUNCT_4:17;
then ( (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = 0 & F . d in {0 } ) by A18, FUNCOP_1:13, FUNCT_1:def 13;
hence (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = F . d by TARSKI:def 1; :: thesis: verum
end;
suppose A19: d in X \ {(P . x2)} ; :: thesis: (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = F . d
then ( d in dom ((X \ {(P . x2)}) --> 1) & d in X & not d in {x1} & X = dom F ) by A13, FUNCT_2:def 1, XBOOLE_0:def 5;
then ( (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = ((X \ {(P . x2)}) --> 1) . d & F . d in rng F & not F . d in {0 } ) by A11, FUNCT_1:def 5, FUNCT_1:def 13, FUNCT_4:14;
then ( (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = 1 & F . d in {0 ,1} & not F . d = 0 ) by A19, FUNCOP_1:13, TARSKI:def 1;
hence (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = F . d by TARSKI:def 2; :: thesis: verum
end;
end;
end;
hence (((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1)) . d = F . d ; :: thesis: verum
end;
then ((P . x2) .--> 0 ) +* ((X \ {(P . x2)}) --> 1) = F by A16, FUNCT_1:9;
hence P1 . x2 = F by A8, A13; :: thesis: verum
end;
hence z in rng P1 by A10, A13, A14, FUNCT_1:def 5; :: thesis: verum
end;
then ( Choose X,1,0 ,1 = rng P1 & cX <> 0 ) by XBOOLE_0:def 10;
then ( P1 is onto & card (Choose X,1,0 ,1) = (card X) choose 1 & card X >= 1 ) by Th18, FUNCT_2:def 3, NAT_1:14;
then A20: ( P1 is onto & card X = card (Choose X,1,0 ,1) & card (card X) = card X ) by NEWTON:33;
then reconsider P1 = P1 as Function of (card (Choose X,1,0 ,1)),(Choose X,1,0 ,1) ;
( P1 is one-to-one & dom Fy = X ) by A1, A20, STIRL2_1:70;
then consider XFS1 being XFinSequence of such that
A21: dom XFS1 = dom P1 and
A22: 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
A23: Card_Intersection Fy,1 = Sum XFS1 by Def4;
XFS = XFS1
proof
( Choose X,1,0 ,1 = {} implies card (Choose X,1,0 ,1) = {} ) ;
then A24: dom P1 = card (Choose X,1,0 ,1) by FUNCT_2:def 1;
then A25: dom XFS1 = dom XFS by A20, A21, FUNCT_2:def 1;
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 A26: z in dom XFS1 ; :: thesis: XFS1 . z = XFS . z
A27: ( P1 . z = H2(z) & H2(z) in Choose X,1,0 ,1 ) by A6, A8, A20, A21, A26;
then consider f being Function of X,{0 ,1} such that
A28: ( f = H2(z) & card (f " {0 }) = 1 ) by Def1;
consider x1 being set such that
A29: f " {0 } = {x1} by A28, CARD_2:60;
( P . z in {(P . z)} & {(P . z)} = dom ((P . z) .--> 0 ) & dom H2(z) = (dom ((P . z) .--> 0 )) \/ (dom ((X \ {(P . z)}) --> 1)) ) by FUNCOP_1:19, FUNCT_4:def 1, TARSKI:def 1;
then ( not P . z in X \ {(P . z)} & P . z in (dom ((P . z) .--> 0 )) \/ (dom ((X \ {(P . z)}) --> 1)) & ((P . z) .--> 0 ) . (P . z) = 0 & dom ((X \ {(P . z)}) --> 1) = X \ {(P . z)} ) by FUNCOP_1:13, FUNCOP_1:19, XBOOLE_0:def 3, XBOOLE_0:def 5;
then ( H2(z) . (P . z) = 0 & P . z in dom H2(z) & 0 in {0 } ) by FUNCT_4:def 1, TARSKI:def 1;
then P . z in f " {0 } by A28, FUNCT_1:def 13;
then ( P . z = x1 & z in dom P & dom P = cX ) by A20, A21, A24, A26, A29, FUNCT_2:def 1, TARSKI:def 1;
then ( card (Intersection Fy,f,0 ) = card (Fy . (P . z)) & XFS1 . z = card (Intersection Fy,f,0 ) & XFS . z = card ((Fy * P) . z) & Fy . (P . z) = (Fy * P) . z ) by A4, A22, A26, A27, A28, A29, Th37, FUNCT_1:23;
hence XFS1 . z = XFS . z ; :: thesis: verum
end;
hence XFS = XFS1 by A25, FUNCT_1:9; :: thesis: verum
end;
hence Card_Intersection Fy,1 = Sum XFS by A23; :: thesis: verum
end;
end;
end;