let X be non empty finite set ; :: thesis: for C being Subset-Family of X st C is (C1) & C is (C2) holds
ex R being DB-Rel st
( the Attributes of R = X & C = candidate-keys (Dependency-str R) )
let C be Subset-Family of X; :: thesis: ( C is (C1) & C is (C2) implies ex R being DB-Rel st
( the Attributes of R = X & C = candidate-keys (Dependency-str R) ) )
assume that
A1: C is (C1) and
A2: C is (C2) ; :: thesis: ex R being DB-Rel st
( the Attributes of R = X & C = candidate-keys (Dependency-str R) )
reconsider D = X --> (bool X) as non-empty 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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((X --> 0) +* (L --> L)) where L is Subset of X : L in M0 } or x in product D )
assume x in { ((X --> 0) +* (L --> L)) where L is Subset of X : L in M0 } ; :: thesis: x in product D
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 ;

A7: now :: thesis: for x being object st x in dom D holds
((X --> 0) +* (L --> L)) . x in D . x

let x be object ; :: thesis: ( x in dom D implies ((X --> 0) +* (L --> L)) . b₁ in D . b₁ )
assume A8: x in dom D ; :: thesis: ((X --> 0) +* (L --> L)) . b₁ in D . b₁
A9: D . x = bool X by A8, FUNCOP_1:7;

per cases ( x in L or not x in L ) ;

suppose A10: x in L ; :: thesis: ((X --> 0) +* (L --> L)) . b₁ in D . b₁

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: verum

end;

suppose not x in L ; :: thesis: ((X --> 0) +* (L --> L)) . b₁ in D . b₁

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: verum

end;

end;

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: verum

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: ( the Attributes of DB = X & C = candidate-keys (Dependency-str DB) )
thus the Attributes of DB = X ; :: thesis: C = candidate-keys (Dependency-str DB)
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: for x being set st x in C holds
x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) }

let x be set ; :: thesis: ( x in C implies x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } )
assume A13: x in C ; :: thesis: x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) }
then reconsider A = x as Subset of X ;
reconsider AA = A, XA = X as Subset of the Attributes of DB by A11;

now :: thesis: for f, g being Element of the Relationship of DB st f | A = g | A holds
f | X = g | X

let f, g be Element of the Relationship of DB; :: thesis: ( f | A = g | A implies b₁ | X = b₂ | X )
assume A14: f | A = g | A ; :: thesis: b₁ | X = b₂ | X
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 ( ( 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 <> {} } ) or ( Lf in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } & Lg = 0 ) or ( Lf = 0 & Lg in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ) or ( Lf = 0 & Lg = 0 ) ) 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: b₁ | X = b₂ | X

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 ( a in Lg or not a in Lg ) ;

suppose A26: a in Lg ; :: thesis: ( g . a = 0 or g . a = Lg )

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: verum

end;

suppose not a in Lg ; :: thesis: ( g . a = 0 or g . a = Lg )

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

end;

end;

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: verum

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: b₁ | X = b₂ | X

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: verum

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: b₁ | X = b₂ | X

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: verum

end;

suppose ( Lf = 0 & Lg = 0 ) ; :: thesis: b₁ | X = b₂ | X

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

end;

end;

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: not a <> A

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

A52: now :: thesis: not a ` = {}

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

end;

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

now :: thesis: for K being Subset of X st K in C holds
not (a `) /\ K = {}

let K be Subset of X; :: thesis: ( K in C implies not (a `) /\ K = {} )
assume A54: K in C ; :: thesis: not (a `) /\ K = {}
assume (a `) /\ K = {} ; :: thesis: contradiction
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: verum

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: ( dom (r0 | a) = (dom r1) /\ a & ( for x being object st x in dom (r0 | a) holds
(r0 | a) . x = r1 . x ) )

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: for x being object st x in dom (r0 | a) holds
(r0 | a) . x = r1 . x
let x be object ; :: thesis: ( x in dom (r0 | a) implies (r0 | a) . x = r1 . x )
assume A60: x in dom (r0 | a) ; :: thesis: (r0 | a) . x = r1 . x
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: verum

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: verum

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: verum

end;

now :: thesis: for x being object holds
( ( x in C implies x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ) & ( x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } implies x in C ) )

let x be object ; :: thesis: ( ( x in C implies x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ) & ( x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } implies x in C ) )
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: ( x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } implies x in C )
assume x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ; :: thesis: x in C
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: for K being set st K in C & K c= A holds
not K <> A

A70: A ^|^ [#] X, Dependency-str DB by A65;
let K be set ; :: thesis: ( K in C & K c= A implies not K <> A )
assume that
A71: K in C and
A72: K c= A ; :: thesis: not K <> A
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: contradiction
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: verum

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: for x being object st x in { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } holds
x in X

let x be object ; :: thesis: ( x in { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } implies x in X )
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: x in X
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: verum

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: contradiction
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: for K being Subset of X st K in C holds
m /\ K <> {}

let K be Subset of X; :: thesis: ( K in C implies m /\ K <> {} )
assume A84: K in C ; :: thesis: m /\ K <> {}
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: verum

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: ( dom (r0 | A) = (dom r1) /\ A & ( for x being object st x in dom (r0 | A) holds
(r0 | A) . x = r1 . x ) )

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: for x being object st x in dom (r0 | A) holds
(r0 | A) . x = r1 . x
A90: dom (r0 | A) = (dom r0) /\ A by RELAT_1:61;
let x be object ; :: thesis: ( x in dom (r0 | A) implies (r0 | A) . x = r1 . x )
assume A91: x in dom (r0 | A) ; :: thesis: (r0 | A) . x = r1 . x

A92: now :: thesis: not x in m

assume x in m ; :: thesis: contradiction
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: verum

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: verum

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: verum

end;

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