let X be non empty finite set ; :: thesis:
let C be Subset-Family of X; :: thesis:
assume that
A1: C is (C1) and
A2: C is (C2) ; :: thesis:
reconsider D = X --> (bool X) as V11() ManySortedSet of X ;
set M = { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ;
reconsider M0 = { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } \/ {0} as non empty set ;
set R = { ((X --> 0) +* (L --> L)) where L is Subset of X : L in M0 } ;
A3: { ((X --> 0) +* (L --> L)) where L is Subset of X : L in M0 } c= product D

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { ((X --> 0) +* (L --> L)) where L is Subset of X : L in M0 } ; :: thesis:
then consider L being Subset of X such that
A5: x = (X --> 0) +* (L --> L) and
L in M0 ;
set g = (X --> 0) +* (L --> L);
A6: dom (L --> L) = L ;

let x be object ; :: thesis:
assume A8: x in dom D ; :: thesis:
A9: D . x = bool X by A8, FUNCOP_1:7;

per cases ;

suppose A10: x in L ; :: thesis:

then ((X --> 0) +* (L --> L)) . x = (L --> L) . x by A6, FUNCT_4:13
.= L by A10, FUNCOP_1:7 ;
hence ((X --> 0) +* (L --> L)) . x in D . x by A9; :: thesis:

end;

suppose not x in L ; :: thesis:

then ((X --> 0) +* (L --> L)) . x = (X --> 0) . x by A6, FUNCT_4:11
.= {} X ;
hence ((X --> 0) +* (L --> L)) . x in D . x by A9; :: thesis:

end;

dom ((X --> 0) +* (L --> L)) = (dom (X --> 0)) \/ L by A6, FUNCT_4:def 1
.= X \/ L
.= X by XBOOLE_1:12 ;
hence x in product D by A5, A7, CARD_3:def 5; :: thesis:

end;

0 in {0} by TARSKI:def 1;
then 0 in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } \/ {0} by XBOOLE_0:def 3;
then (X --> 0) +* (({} X) --> ({} X)) in { ((X --> 0) +* (L --> L)) where L is Subset of X : L in M0 } ;
then reconsider R = { ((X --> 0) +* (L --> L)) where L is Subset of X : L in M0 } as non empty Subset of (product D) by A3;
take DB = DB-Rel(# X,D,R #); :: thesis:
thus the Attributes of DB = X ; :: thesis:
set ds = Dependency-str DB;
set ck = { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ;
A11: [#] X = X ;

A12: now :: thesis:

let x be set ; :: thesis:
assume A13: x in C ; :: thesis:
then reconsider A = x as Subset of X ;
reconsider AA = A, XA = X as Subset of the Attributes of DB by A11;

now :: thesis:

let f, g be Element of the Relationship of DB; :: thesis:
assume A14: f | A = g | A ; :: thesis:
f in R ;
then consider Lf being Subset of X such that
A15: f = (X --> 0) +* (Lf --> Lf) and
A16: Lf in M0 ;
A17: ( Lf in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } or Lf in {0} ) by A16, XBOOLE_0:def 3;
A18: dom (Lf --> Lf) = Lf ;
g in R ;
then consider Lg being Subset of X such that
A19: g = (X --> 0) +* (Lg --> Lg) and
A20: Lg in M0 ;
A21: ( Lg in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } or Lg in {0} ) by A20, XBOOLE_0:def 3;
A22: dom (Lg --> Lg) = Lg ;

per cases by A17, A21, TARSKI:def 1;

suppose ( Lf in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } & Lg in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ) ; :: thesis:

then ex Lff being Subset of X st
( Lf = Lff & ( for K being Subset of X st K in C holds
Lff /\ K <> {} ) ) ;
then A23: Lf /\ A <> {} by A13;
then consider a being object such that
A24: a in Lf /\ A by XBOOLE_0:def 1;
A25: ( g . a = 0 or g . a = Lg )

proof

per cases ;

suppose A26: a in Lg ; :: thesis:

then g . a = (Lg --> Lg) . a by A19, A22, FUNCT_4:13;
hence ( g . a = 0 or g . a = Lg ) by A26, FUNCOP_1:7; :: thesis:

end;

suppose not a in Lg ; :: thesis:

then g . a = (X --> 0) . a by A19, A22, FUNCT_4:11;
hence ( g . a = 0 or g . a = Lg ) ; :: thesis:

end;

A27: a in Lf by A24, XBOOLE_0:def 4;
A28: a in A by A24, XBOOLE_0:def 4;
then A29: (g | A) . a = g . a by FUNCT_1:49;
(f | A) . a = f . a by A28, FUNCT_1:49
.= (Lf --> Lf) . a by A15, A18, A27, FUNCT_4:13
.= Lf by A27, FUNCOP_1:7 ;
hence f | X = g | X by A14, A15, A19, A23, A29, A25; :: thesis:

end;

suppose A30: ( Lf in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } & Lg = 0 ) ; :: thesis:

then ex L being Subset of X st
( Lf = L & ( for K being Subset of X st K in C holds
L /\ K <> {} ) ) ;
then A31: Lf /\ A <> {} by A13;
then consider a being object such that
A32: a in Lf /\ A by XBOOLE_0:def 1;
A33: a in A by A32, XBOOLE_0:def 4;
then A34: (g | A) . a = g . a by FUNCT_1:49
.= ((X --> 0) +* {}) . a by A19, A30
.= (X --> 0) . a
.= {} ;
A35: a in Lf by A32, XBOOLE_0:def 4;
(f | A) . a = f . a by A33, FUNCT_1:49
.= (Lf --> Lf) . a by A15, A18, A35, FUNCT_4:13
.= Lf by A35, FUNCOP_1:7 ;
hence f | X = g | X by A14, A31, A34; :: thesis:

end;

suppose A36: ( Lf = 0 & Lg in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ) ; :: thesis:

then ex L being Subset of X st
( Lg = L & ( for K being Subset of X st K in C holds
L /\ K <> {} ) ) ;
then A37: Lg /\ A <> {} by A13;
then consider a being object such that
A38: a in Lg /\ A by XBOOLE_0:def 1;
A39: a in A by A38, XBOOLE_0:def 4;
then A40: (f | A) . a = f . a by FUNCT_1:49
.= ((X --> 0) +* {}) . a by A15, A36
.= (X --> 0) . a
.= {} ;
A41: a in Lg by A38, XBOOLE_0:def 4;
(g | A) . a = g . a by A39, FUNCT_1:49
.= (Lg --> Lg) . a by A19, A22, A41, FUNCT_4:13
.= Lg by A41, FUNCOP_1:7 ;
hence f | X = g | X by A14, A37, A40; :: thesis:

end;

suppose ( Lf = 0 & Lg = 0 ) ; :: thesis:

hence f | X = g | X by A15, A19; :: thesis:

end;

then AA >|> XA,DB ;
then [A,X] in Dependency-str DB ;
then consider a, b being Subset of X such that
A42: [a,b] in Maximal_wrt (Dependency-str DB) and
A43: [a,b] >= [A,([#] X)] by Th26;
A44: a c= A by A43;
[a,b] in Dependency-str DB by A42;
then consider aa, XX being Subset of the Attributes of DB such that
A45: [a,b] = [aa,XX] and
A46: aa >|> XX,DB ;
A47: a = aa by A45, XTUPLE_0:1;
A48: b = XX by A45, XTUPLE_0:1;
A49: X c= b by A43;
then A50: b = X by XBOOLE_0:def 10;

now :: thesis:

set r1 = (X --> 0) +* ((a `) --> (a `));
set r0 = X --> 0;
assume A51: a <> A ; :: thesis:

A52: now :: thesis:

assume a ` = {} ; :: thesis:
then a ` c= a ;
then a = X by A11, SUBSET_1:19;
hence contradiction by A44, A51, XBOOLE_0:def 10; :: thesis:

end;

then consider y being object such that
A53: y in a ` by XBOOLE_0:def 1;

now :: thesis:

let K be Subset of X; :: thesis:
assume A54: K in C ; :: thesis:
assume (a `) /\ K = {} ; :: thesis:
then K misses a ` by XBOOLE_0:def 7;
then A55: K c= a by SUBSET_1:24;
then K c= A by A44;
then K = A by A2, A13, A54;
hence contradiction by A44, A51, A55, XBOOLE_0:def 10; :: thesis:

end;

then a ` in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ;
then a ` in M0 by XBOOLE_0:def 3;
then A56: (X --> 0) +* ((a `) --> (a `)) in R ;
0 in {0} by TARSKI:def 1;
then 0 in M0 by XBOOLE_0:def 3;
then (X --> 0) +* (({} X) --> ({} X)) in R ;
then (X --> 0) +* {} in R ;
then reconsider r0 = X --> 0, r1 = (X --> 0) +* ((a `) --> (a `)) as Element of the Relationship of DB by A56;
A57: (r0 | X) . y = r0 . y
.= 0 ;
A58: dom ((a `) --> (a `)) = a ` ;

now :: thesis:

A59: dom r1 = (dom (X --> 0)) \/ (dom ((a `) --> (a `))) by FUNCT_4:def 1
.= X \/ (dom ((a `) --> (a `)))
.= X \/ (a `)
.= X by XBOOLE_1:12 ;
dom r0 = X ;
hence dom (r0 | a) = (dom r1) /\ a by A59, RELAT_1:61; :: thesis:
let x be object ; :: thesis:
assume A60: x in dom (r0 | a) ; :: thesis:
dom (r0 | a) = (dom r0) /\ a by RELAT_1:61;
then A61: x in a by A60, XBOOLE_0:def 4;
a misses a ` by XBOOLE_1:79;
then a /\ (a `) = {} by XBOOLE_0:def 7;
then A62: not x in a ` by A61, XBOOLE_0:def 4;
thus (r0 | a) . x = (X --> 0) . x by A61, FUNCT_1:49
.= r1 . x by A58, A62, FUNCT_4:11 ; :: thesis:

end;

then A63: r0 | a = r1 | a by FUNCT_1:46;
(r1 | X) . y = r1 . y by A53, FUNCT_1:49
.= ((a `) --> (a `)) . y by A58, A53, FUNCT_4:13
.= a ` by A53, FUNCOP_1:7 ;
hence contradiction by A50, A46, A47, A48, A63, A52, A57; :: thesis:

end;

then [A,X] in Maximal_wrt (Dependency-str DB) by A42, A49, XBOOLE_0:def 10;
hence x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
thus ( x in C implies x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ) by A12; :: thesis:
assume x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ; :: thesis:
then consider A being Subset of X such that
A64: x = A and
A65: [A,X] in Maximal_wrt (Dependency-str DB) ;
[A,X] in Dependency-str DB by A65;
then consider aa, XX being Subset of the Attributes of DB such that
A66: [A,X] = [aa,XX] and
A67: aa >|> XX,DB ;
A68: X = XX by A66, XTUPLE_0:1;

A69: now :: thesis:

A70: A ^|^ [#] X, Dependency-str DB by A65;
let K be set ; :: thesis:
assume that
A71: K in C and
A72: K c= A ; :: thesis:
K in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } by A12, A71;
then consider B being Subset of X such that
A73: K = B and
A74: [B,X] in Maximal_wrt (Dependency-str DB) ;
assume A75: K <> A ; :: thesis:
reconsider AA = A, B = B, XA = X as Subset of the Attributes of DB by A11;
[AA,XA] <= [B,XA] by A72, A73;
hence contradiction by A73, A74, A75, A70, Th27; :: thesis:

end;

set m = { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } ;

A76: now :: thesis:

let x be object ; :: thesis:
assume x in { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } ; :: thesis:
then ex a being Element of X st
( x = a & not a in A & ex K being set st
( K in C & a in K ) ) ;
hence x in X ; :: thesis:

end;

consider K being object such that
A77: K in C by A1, XBOOLE_0:def 1;
reconsider K = K as Subset of X by A77;
A78: A = aa by A66, XTUPLE_0:1;
assume A79: not x in C ; :: thesis:
then not K c= A by A64, A69, A77;
then consider k being object such that
A80: k in K and
A81: not k in A ;
reconsider k = k as Element of X by A80;
A82: k in { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } by A77, A80, A81;
then consider n being object such that
A83: n in { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } ;
reconsider m = { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } as Subset of X by A76, TARSKI:def 3;
set r0 = X --> 0;
set r1 = (X --> 0) +* (m --> m);

now :: thesis:

let K be Subset of X; :: thesis:
assume A84: K in C ; :: thesis:
not K c= A by A64, A69, A79, A84;
then consider k being object such that
A85: k in K and
A86: not k in A ;
k in m by A84, A85, A86;
hence m /\ K <> {} by A85, XBOOLE_0:def 4; :: thesis:

end;

then m in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ;
then m in M0 by XBOOLE_0:def 3;
then A87: (X --> 0) +* (m --> m) in R ;
0 in {0} by TARSKI:def 1;
then 0 in M0 by XBOOLE_0:def 3;
then (X --> 0) +* (({} X) --> ({} X)) in R ;
then (X --> 0) +* {} in R ;
then reconsider r0 = X --> 0, r1 = (X --> 0) +* (m --> m) as Element of the Relationship of DB by A87;
A88: dom (m --> m) = m ;

now :: thesis:

A89: dom r1 = (dom (X --> 0)) \/ (dom (m --> m)) by FUNCT_4:def 1
.= X \/ (dom (m --> m))
.= X \/ m
.= X by XBOOLE_1:12 ;
dom r0 = X ;
hence dom (r0 | A) = (dom r1) /\ A by A89, RELAT_1:61; :: thesis:
A90: dom (r0 | A) = (dom r0) /\ A by RELAT_1:61;
let x be object ; :: thesis:
assume A91: x in dom (r0 | A) ; :: thesis:

A92: now :: thesis:

assume x in m ; :: thesis:
then ex a being Element of X st
( x = a & not a in A & ex K being set st
( K in C & a in K ) ) ;
hence contradiction by A90, A91, XBOOLE_0:def 4; :: thesis:

end;

x in A by A90, A91, XBOOLE_0:def 4;
hence (r0 | A) . x = (X --> 0) . x by FUNCT_1:49
.= r1 . x by A88, A92, FUNCT_4:11 ;
:: thesis:

end;

then A93: r0 | A = r1 | A by FUNCT_1:46;
A94: (r1 | X) . n = r1 . n by A83, FUNCT_1:49
.= (m --> m) . n by A83, A88, FUNCT_4:13
.= m by A83, FUNCOP_1:7 ;
(r0 | X) . n = r0 . n
.= 0 ;
hence contradiction by A82, A93, A67, A78, A68, A94; :: thesis:

end;

hence C = candidate-keys (Dependency-str DB) by TARSKI:2; :: thesis: