let X be non empty finite set ; :: thesis: for F being Full-family of X ex R being DB-Rel st
( the Attributes of R = X & ( for a being Element of X holds the Domains of R . a = INT ) & F = Dependency-str R )
let F be Full-family of X; :: thesis: ex R being DB-Rel st
( the Attributes of R = X & ( for a being Element of X holds the Domains of R . a = INT ) & F = Dependency-str R )
reconsider D = X --> INT as non-empty ManySortedSet of X ;
consider G being Subset-Family of X such that
G is_generator-set_of saturated-subsets F and
A1: F = X deps_encl_by G by Th43;
consider H being FinSequence such that
A2: rng H = G and
H is one-to-one by FINSEQ_4:58;

A4: now :: thesis: ( dom (X --> 0) = dom D & ( for x being object st x in dom D holds
(X --> 0) . x in D . x ) )

set f = X --> 0;
thus dom (X --> 0) = dom D ; :: thesis: for x being object st x in dom D holds
(X --> 0) . x in D . x
let x be object ; :: thesis: ( x in dom D implies (X --> 0) . x in D . x )
assume A5: x in dom D ; :: thesis: (X --> 0) . x in D . x
then (X --> 0) . x = 0 by FUNCOP_1:7;
then (X --> 0) . x in NAT ;
then (X --> 0) . x in INT by NUMBERS:17;
hence (X --> 0) . x in D . x by A5, FUNCOP_1:7; :: thesis: verum

end;

then A6: X --> 0 is Element of product D by CARD_3:def 5;
reconsider H = H as FinSequence of G by A2, FINSEQ_1:def 4;

per cases ( G is empty or not G is empty ) ;

suppose A7: G is empty ; :: thesis: ex R being DB-Rel st
( the Attributes of R = X & ( for a being Element of X holds the Domains of R . a = INT ) & F = Dependency-str R )

set R = {(X --> 0)};
{(X --> 0)} c= product D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(X --> 0)} or x in product D )
assume x in {(X --> 0)} ; :: thesis: x in product D
then x = X --> 0 by TARSKI:def 1;
hence x in product D by A4, CARD_3:def 5; :: thesis: verum

end;

then reconsider R = {(X --> 0)} as non empty Subset of (product D) ;
set BD = DB-Rel(# X,D,R #);
take DB-Rel(# X,D,R #) ; :: thesis: ( the Attributes of DB-Rel(# X,D,R #) = X & ( for a being Element of X holds the Domains of DB-Rel(# X,D,R #) . a = INT ) & F = Dependency-str DB-Rel(# X,D,R #) )
thus ( the Attributes of DB-Rel(# X,D,R #) = X & ( for a being Element of X holds the Domains of DB-Rel(# X,D,R #) . a = INT ) ) ; :: thesis: F = Dependency-str DB-Rel(# X,D,R #)
set Ds = Dependency-str DB-Rel(# X,D,R #);

now :: thesis: for x being object holds
( ( x in F implies x in Dependency-str DB-Rel(# X,D,R #) ) & ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F ) )

let x be object ; :: thesis: ( ( x in F implies x in Dependency-str DB-Rel(# X,D,R #) ) & ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F ) )

hereby :: thesis: ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F )

assume x in F ; :: thesis: x in Dependency-str DB-Rel(# X,D,R #)
then consider A, B being Subset of X such that
A8: x = [A,B] and
for g being set st g in G & A c= g holds
B c= g by A1;
reconsider A = A, B = B as Subset of the Attributes of DB-Rel(# X,D,R #) ;
A >|> B, DB-Rel(# X,D,R #)

proof

let f, g be Element of the Relationship of DB-Rel(# X,D,R #); :: according to ARMSTRNG:def 7 :: thesis: ( f | A = g | A implies f | B = g | B )
f = X --> 0 by TARSKI:def 1;
hence ( f | A = g | A implies f | B = g | B ) by TARSKI:def 1; :: thesis: verum

end;

hence x in Dependency-str DB-Rel(# X,D,R #) by A8; :: thesis: verum

end;

assume x in Dependency-str DB-Rel(# X,D,R #) ; :: thesis: x in F
then consider A, B being Subset of the Attributes of DB-Rel(# X,D,R #) such that
A9: x = [A,B] and
A >|> B, DB-Rel(# X,D,R #) ;
for g being set st g in G & A c= g holds
B c= g by A7;
hence x in F by A1, A9; :: thesis: verum

end;

hence F = Dependency-str DB-Rel(# X,D,R #) by TARSKI:2; :: thesis: verum

end;

suppose A10: not G is empty ; :: thesis: ex R being DB-Rel st
( the Attributes of R = X & ( for a being Element of X holds the Domains of R . a = INT ) & F = Dependency-str R )

then not H is empty by A2;
then reconsider n = len H as non zero Element of NAT ;
defpred S₁[ set , Element of n -tuples_on BOOLEAN] means for i being Element of NAT st i in Seg n holds
( ( $1 in H . i implies $2 . i = 0 ) & ( not $1 in H . i implies $2 . i = 1 ) );

A11: now :: thesis: for x being Element of X ex y being Element of n -tuples_on BOOLEAN st S₁[x,y]

let x be Element of X; :: thesis: ex y being Element of n -tuples_on BOOLEAN st S₁[x,y]
defpred S₂[ set , set ] means ( ( x in H . $1 implies $2 = 0 ) & ( not x in H . $1 implies $2 = 1 ) );
A12: for i being Nat st i in Seg n holds
ex x being Element of BOOLEAN st S₂[i,x]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex x being Element of BOOLEAN st S₂[i,x] )
assume i in Seg n ; :: thesis: ex x being Element of BOOLEAN st S₂[i,x]

per cases ( x in H . i or not x in H . i ) ;

suppose A13: x in H . i ; :: thesis: ex x being Element of BOOLEAN st S₂[i,x]

reconsider b = FALSE as Element of BOOLEAN ;
take b ; :: thesis: S₂[i,b]
thus S₂[i,b] by A13; :: thesis: verum

end;

suppose A14: not x in H . i ; :: thesis: ex x being Element of BOOLEAN st S₂[i,x]

reconsider b = TRUE as Element of BOOLEAN ;
take b ; :: thesis: S₂[i,b]
thus S₂[i,b] by A14; :: thesis: verum

end;

end;

end;

consider y being FinSequence of BOOLEAN such that
A15: dom y = Seg n and
A16: for i being Nat st i in Seg n holds
S₂[i,y . i] from FINSEQ_1:sch 5(A12);
A17: y in BOOLEAN * by FINSEQ_1:def 11;
len y = n by A15, FINSEQ_1:def 3;
then y in { s where s is Element of BOOLEAN * : len s = n } by A17;
then reconsider y = y as Element of n -tuples_on BOOLEAN ;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] by A16; :: thesis: verum

end;

consider M being Function of X,(n -tuples_on BOOLEAN) such that
A18: for x being Element of X holds S₁[x,M . x] from FUNCT_2:sch 3(A11);
set R = { f where f is Element of product D : ex i being Element of NAT st
for x being Element of X holds f . x = Absval ((n -BinarySequence i) '&' (M . x)) } ;
A19: { f where f is Element of product D : ex i being Element of NAT st
for x being Element of X holds f . x = Absval ((n -BinarySequence i) '&' (M . x)) } c= product D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Element of product D : ex i being Element of NAT st
for x being Element of X holds f . x = Absval ((n -BinarySequence i) '&' (M . x)) } or x in product D )
assume x in { f where f is Element of product D : ex i being Element of NAT st
for x being Element of X holds f . x = Absval ((n -BinarySequence i) '&' (M . x)) } ; :: thesis: x in product D
then ex f being Element of product D st
( x = f & ex i being Element of NAT st
for x being Element of X holds f . x = Absval ((n -BinarySequence i) '&' (M . x)) ) ;
hence x in product D ; :: thesis: verum

end;

now :: thesis: ex i being Element of NAT st
for x being Element of X holds (X --> 0) . x = Absval ((n -BinarySequence i) '&' (M . x))

take i = 0 ; :: thesis: for x being Element of X holds (X --> 0) . x = Absval ((n -BinarySequence i) '&' (M . x))
set f = X --> 0;
let x be Element of X; :: thesis: (X --> 0) . x = Absval ((n -BinarySequence i) '&' (M . x))
A20: (n -BinarySequence i) '&' (M . x) = n -BinarySequence i by Th5
.= 0* n by BINARI_3:25 ;
thus (X --> 0) . x = 0
.= Absval ((n -BinarySequence i) '&' (M . x)) by A20, BINARI_3:6 ; :: thesis: verum

end;

then X --> 0 in { f where f is Element of product D : ex i being Element of NAT st
for x being Element of X holds f . x = Absval ((n -BinarySequence i) '&' (M . x)) } by A6;
then reconsider R = { f where f is Element of product D : ex i being Element of NAT st
for x being Element of X holds f . x = Absval ((n -BinarySequence i) '&' (M . x)) } as non empty Subset of (product D) by A19;
set BD = DB-Rel(# X,D,R #);
take DB-Rel(# X,D,R #) ; :: thesis: ( the Attributes of DB-Rel(# X,D,R #) = X & ( for a being Element of X holds the Domains of DB-Rel(# X,D,R #) . a = INT ) & F = Dependency-str DB-Rel(# X,D,R #) )
thus ( the Attributes of DB-Rel(# X,D,R #) = X & ( for a being Element of X holds the Domains of DB-Rel(# X,D,R #) . a = INT ) ) ; :: thesis: F = Dependency-str DB-Rel(# X,D,R #)
set Ds = Dependency-str DB-Rel(# X,D,R #);
A21: dom H = Seg n by FINSEQ_1:def 3;

now :: thesis: for x being object holds
( ( x in F implies x in Dependency-str DB-Rel(# X,D,R #) ) & ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F ) )

let x be object ; :: thesis: ( ( x in F implies x in Dependency-str DB-Rel(# X,D,R #) ) & ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F ) )

hereby :: thesis: ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F )

assume x in F ; :: thesis: x in Dependency-str DB-Rel(# X,D,R #)
then consider A, B being Subset of X such that
A22: x = [A,B] and
A23: for g being set st g in G & A c= g holds
B c= g by A1;
reconsider A9 = A, B9 = B as Subset of the Attributes of DB-Rel(# X,D,R #) ;
A9 >|> B9, DB-Rel(# X,D,R #)

proof

let f, g be Element of the Relationship of DB-Rel(# X,D,R #); :: according to ARMSTRNG:def 7 :: thesis: ( f | A9 = g | A9 implies f | B9 = g | B9 )
assume A24: f | A9 = g | A9 ; :: thesis: f | B9 = g | B9
f in R ;
then consider Rf being Element of product D such that
A25: f = Rf and
A26: ex i being Element of NAT st
for x being Element of X holds Rf . x = Absval ((n -BinarySequence i) '&' (M . x)) ;
consider fi being Element of NAT such that
A27: for x being Element of X holds Rf . x = Absval ((n -BinarySequence fi) '&' (M . x)) by A26;
g in R ;
then consider Rg being Element of product D such that
A28: g = Rg and
A29: ex i being Element of NAT st
for x being Element of X holds Rg . x = Absval ((n -BinarySequence i) '&' (M . x)) ;
consider gi being Element of NAT such that
A30: for x being Element of X holds Rg . x = Absval ((n -BinarySequence gi) '&' (M . x)) by A29;
A31: dom g = dom D by A28, CARD_3:9
.= dom f by A25, CARD_3:9 ;

now :: thesis: ( dom (g | B) = (dom f) /\ B & ( for a being object st a in dom (g | B) holds
(g | B) . a = f . a ) )

set nbg = n -BinarySequence gi;
set nbf = n -BinarySequence fi;
thus A32: dom (g | B) = (dom f) /\ B by A31, RELAT_1:61; :: thesis: for a being object st a in dom (g | B) holds
(g | B) . a = f . a
let a be object ; :: thesis: ( a in dom (g | B) implies (g | B) . a = f . a )
assume A33: a in dom (g | B) ; :: thesis: (g | B) . a = f . a
reconsider x = a as Element of X by A32, A33;
reconsider Mx = M . x as Tuple of n,BOOLEAN ;
set ng = (n -BinarySequence gi) '&' (M . x);
set nf = (n -BinarySequence fi) '&' (M . x);
A34: dom (M . x) = Seg n by Lm2;
A35: dom ((n -BinarySequence fi) '&' (M . x)) = Seg n by Lm1;
A36: a in B by A32, A33, XBOOLE_0:def 4;

now :: thesis: ( dom ((n -BinarySequence fi) '&' (M . x)) = dom ((n -BinarySequence gi) '&' (M . x)) & ( for i being object st i in dom ((n -BinarySequence fi) '&' (M . x)) holds
((n -BinarySequence fi) '&' (M . x)) . i = ((n -BinarySequence gi) '&' (M . x)) . i ) )

thus dom ((n -BinarySequence fi) '&' (M . x)) = dom ((n -BinarySequence gi) '&' (M . x)) by A35, Lm1; :: thesis: for i being object st i in dom ((n -BinarySequence fi) '&' (M . x)) holds
((n -BinarySequence fi) '&' (M . x)) . b₂ = ((n -BinarySequence gi) '&' (M . x)) . b₂
let i be object ; :: thesis: ( i in dom ((n -BinarySequence fi) '&' (M . x)) implies ((n -BinarySequence fi) '&' (M . x)) . b₁ = ((n -BinarySequence gi) '&' (M . x)) . b₁ )
assume A37: i in dom ((n -BinarySequence fi) '&' (M . x)) ; :: thesis: ((n -BinarySequence fi) '&' (M . x)) . b₁ = ((n -BinarySequence gi) '&' (M . x)) . b₁

per cases ( A c= H . i or not A c= H . i ) ;

suppose A c= H . i ; :: thesis: ((n -BinarySequence fi) '&' (M . x)) . b₁ = ((n -BinarySequence gi) '&' (M . x)) . b₁

then A38: B c= H . i by A2, A21, A23, A35, A37, FUNCT_1:3;
A39: Mx /. i = Mx . i by A34, A35, A37, PARTFUN1:def 6
.= 0 by A18, A36, A35, A37, A38 ;
thus ((n -BinarySequence fi) '&' (M . x)) . i = ((n -BinarySequence fi) /. i) '&' (Mx /. i) by A35, A37, Def5
.= ((n -BinarySequence gi) /. i) '&' (Mx /. i) by A39
.= ((n -BinarySequence gi) '&' (M . x)) . i by A35, A37, Def5 ; :: thesis: verum

end;

suppose A40: not A c= H . i ; :: thesis: ((n -BinarySequence fi) '&' (M . x)) . b₁ = ((n -BinarySequence gi) '&' (M . x)) . b₁

thus ((n -BinarySequence fi) '&' (M . x)) . i = ((n -BinarySequence gi) '&' (M . x)) . i :: thesis: verum

proof

consider xx being object such that
A41: xx in A and
A42: not xx in H . i by A40;
reconsider xx = xx as Element of X by A41;
A43: f . xx = (g | A) . xx by A24, A41, FUNCT_1:49
.= g . xx by A41, FUNCT_1:49 ;
reconsider Mxx = M . xx as Tuple of n,BOOLEAN ;
A44: f . xx = Absval ((n -BinarySequence fi) '&' (M . xx)) by A25, A27;
A45: g . xx = Absval ((n -BinarySequence gi) '&' (M . xx)) by A28, A30;
dom (M . xx) = Seg n by Lm2;
then A46: Mxx /. i = Mxx . i by A35, A37, PARTFUN1:def 6
.= 1 by A18, A35, A37, A42 ;
then A47: (n -BinarySequence fi) /. i = ((n -BinarySequence fi) /. i) '&' (Mxx /. i)
.= ((n -BinarySequence fi) '&' (M . xx)) . i by A35, A37, Def5
.= ((n -BinarySequence gi) '&' (M . xx)) . i by A43, A44, A45, BINARI_3:2
.= ((n -BinarySequence gi) /. i) '&' (Mxx /. i) by A35, A37, Def5
.= (n -BinarySequence gi) /. i by A46 ;
thus ((n -BinarySequence fi) '&' (M . x)) . i = ((n -BinarySequence fi) /. i) '&' (Mx /. i) by A35, A37, Def5
.= ((n -BinarySequence gi) '&' (M . x)) . i by A35, A37, A47, Def5 ; :: thesis: verum

end;

end;

end;

end;

then (n -BinarySequence fi) '&' (M . x) = (n -BinarySequence gi) '&' (M . x) by FUNCT_1:2;
then g . a = Absval ((n -BinarySequence fi) '&' (M . x)) by A28, A30
.= f . a by A25, A27 ;
hence (g | B) . a = f . a by A33, FUNCT_1:47; :: thesis: verum

end;

hence f | B9 = g | B9 by FUNCT_1:46; :: thesis: verum

end;

hence x in Dependency-str DB-Rel(# X,D,R #) by A22; :: thesis: verum

end;

assume x in Dependency-str DB-Rel(# X,D,R #) ; :: thesis: x in F
then consider A, B being Subset of the Attributes of DB-Rel(# X,D,R #) such that
A48: x = [A,B] and
A49: A >|> B, DB-Rel(# X,D,R #) ;

now :: thesis: for gg being set st gg in G & A c= gg holds
B c= gg

deffunc H₁( Element of X) -> Element of NAT = Absval ((n -BinarySequence 0) '&' (M . $1));
let gg be set ; :: thesis: ( gg in G & A c= gg implies B c= gg )
assume that
A50: gg in G and
A51: A c= gg and
A52: not B c= gg ; :: thesis: contradiction
reconsider gg = gg as Element of G by A50;
consider f being Function of X,NAT such that
A53: for x being Element of X holds f . x = H₁(x) from FUNCT_2:sch 4();

A54: now :: thesis: for x being object st x in dom D holds
f . x in D . x

let x be object ; :: thesis: ( x in dom D implies f . x in D . x )
assume x in dom D ; :: thesis: f . x in D . x
then reconsider x9 = x as Element of X ;
f . x9 in INT by NUMBERS:17;
hence f . x in D . x ; :: thesis: verum

end;

A55: dom f = dom D by FUNCT_2:def 1;
then reconsider f = f as Element of product D by A54, CARD_3:def 5;
consider i being Nat such that
A56: i in dom H and
A57: H . i = gg by A2, A10, FINSEQ_2:10;
i <> 0 by A21, A56, FINSEQ_1:1;
then consider k being Nat such that
A58: i = k + 1 by NAT_1:6;
consider bx being object such that
A59: bx in B and
A60: not bx in gg by A52;
reconsider bx = bx as Element of X by A59;
reconsider Mbx = M . bx as Tuple of n,BOOLEAN ;
A61: f in R by A53;
dom Mbx = Seg n by Lm1;
then A62: Mbx /. i = Mbx . i by A21, A56, PARTFUN1:def 6
.= 1 by A21, A18, A60, A56, A57 ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
deffunc H₂( Element of X) -> Element of NAT = Absval ((n -BinarySequence (2 to_power k)) '&' (M . $1));
consider g being Function of X,NAT such that
A63: for x being Element of X holds g . x = H₂(x) from FUNCT_2:sch 4();

A64: now :: thesis: for x being object st x in dom D holds
g . x in D . x

let x be object ; :: thesis: ( x in dom D implies g . x in D . x )
assume x in dom D ; :: thesis: g . x in D . x
then reconsider x9 = x as Element of X ;
g . x9 in INT by NUMBERS:17;
hence g . x in D . x ; :: thesis: verum

end;

A65: dom g = dom D by FUNCT_2:def 1;
then reconsider g = g as Element of product D by A64, CARD_3:def 5;
i <= n by A21, A56, FINSEQ_1:1;
then A66: k < n by A58, NAT_1:13;

now :: thesis: ( dom (f | A) = (dom g) /\ A & ( for x being object st x in dom (f | A) holds
(f | A) . x = g . x ) )

thus A67: dom (f | A) = (dom g) /\ A by A55, A65, RELAT_1:61; :: thesis: for x being object st x in dom (f | A) holds
(f | A) . x = g . x
let x be object ; :: thesis: ( x in dom (f | A) implies (f | A) . x = g . x )
assume A68: x in dom (f | A) ; :: thesis: (f | A) . x = g . x
then reconsider a = x as Element of X by A67;
set bs0 = n -BinarySequence 0;
set bsi = n -BinarySequence (2 to_power k);
A69: g . a = Absval ((n -BinarySequence (2 to_power k)) '&' (M . a)) by A63;
set L = (n -BinarySequence 0) '&' (M . a);
set R = (n -BinarySequence (2 to_power k)) '&' (M . a);
reconsider Ma = M . a as Tuple of n,BOOLEAN ;
A70: x in A by A68;

A71: now :: thesis: ( dom ((n -BinarySequence 0) '&' (M . a)) = dom ((n -BinarySequence (2 to_power k)) '&' (M . a)) & ( for j being object st j in dom ((n -BinarySequence 0) '&' (M . a)) holds
((n -BinarySequence 0) '&' (M . a)) . j = ((n -BinarySequence (2 to_power k)) '&' (M . a)) . j ) )

thus dom ((n -BinarySequence 0) '&' (M . a)) = Seg n by Lm1
.= dom ((n -BinarySequence (2 to_power k)) '&' (M . a)) by Lm1 ; :: thesis: for j being object st j in dom ((n -BinarySequence 0) '&' (M . a)) holds
((n -BinarySequence 0) '&' (M . a)) . b₂ = ((n -BinarySequence (2 to_power k)) '&' (M . a)) . b₂
let j be object ; :: thesis: ( j in dom ((n -BinarySequence 0) '&' (M . a)) implies ((n -BinarySequence 0) '&' (M . a)) . b₁ = ((n -BinarySequence (2 to_power k)) '&' (M . a)) . b₁ )
A72: n -BinarySequence 0 = 0* n by BINARI_3:25
.= n |-> 0 by EUCLID:def 4 ;
assume A73: j in dom ((n -BinarySequence 0) '&' (M . a)) ; :: thesis: ((n -BinarySequence 0) '&' (M . a)) . b₁ = ((n -BinarySequence (2 to_power k)) '&' (M . a)) . b₁
then reconsider nj = j as Element of NAT ;
A74: j in Seg n by A73, Lm1;
dom (n -BinarySequence 0) = Seg n by Lm1;
then A75: (n -BinarySequence 0) /. nj = (n -BinarySequence 0) . nj by A74, PARTFUN1:def 6
.= 0 by A72 ;
A76: ((n -BinarySequence 0) '&' (M . a)) . j = ((n -BinarySequence 0) /. nj) '&' (Ma /. nj) by A74, Def5
.= 0 by A75 ;

per cases ( i <> nj or i = nj ) ;

suppose A77: i <> nj ; :: thesis: ((n -BinarySequence 0) '&' (M . a)) . b₁ = ((n -BinarySequence (2 to_power k)) '&' (M . a)) . b₁

dom (n -BinarySequence (2 to_power k)) = Seg n by Lm1;
then A78: (n -BinarySequence (2 to_power k)) /. nj = (n -BinarySequence (2 to_power k)) . nj by A74, PARTFUN1:def 6
.= FALSE by A58, A66, A74, A77, Th7 ;
((n -BinarySequence (2 to_power k)) '&' (M . a)) . j = ((n -BinarySequence (2 to_power k)) /. nj) '&' (Ma /. nj) by A74, Def5;
hence ((n -BinarySequence 0) '&' (M . a)) . j = ((n -BinarySequence (2 to_power k)) '&' (M . a)) . j by A76, A78; :: thesis: verum

end;

suppose A79: i = nj ; :: thesis: ((n -BinarySequence 0) '&' (M . a)) . b₁ = ((n -BinarySequence (2 to_power k)) '&' (M . a)) . b₁

dom Ma = Seg n by Lm1;
then A80: Ma /. nj = Ma . i by A74, A79, PARTFUN1:def 6
.= 0 by A18, A51, A57, A70, A74, A79 ;
((n -BinarySequence (2 to_power k)) '&' (M . a)) . j = ((n -BinarySequence (2 to_power k)) /. nj) '&' (Ma /. nj) by A74, Def5
.= 0 by A80 ;
hence ((n -BinarySequence 0) '&' (M . a)) . j = ((n -BinarySequence (2 to_power k)) '&' (M . a)) . j by A76; :: thesis: verum

end;

end;

end;

(f | A) . a = f . a by A68, FUNCT_1:49
.= Absval ((n -BinarySequence 0) '&' (M . a)) by A53 ;
hence (f | A) . x = g . x by A69, A71, FUNCT_1:2; :: thesis: verum

end;

then A81: f | A = g | A by FUNCT_1:46;
set bs0 = n -BinarySequence 0;
set bsi = n -BinarySequence (2 to_power k);
A82: n -BinarySequence 0 = 0* n by BINARI_3:25
.= n |-> 0 by EUCLID:def 4 ;
dom (n -BinarySequence 0) = Seg n by Lm1;
then A83: (n -BinarySequence 0) /. i = (n -BinarySequence 0) . i by A21, A56, PARTFUN1:def 6
.= 0 by A82 ;
dom (n -BinarySequence (2 to_power k)) = Seg n by Lm1;
then A84: (n -BinarySequence (2 to_power k)) /. i = (n -BinarySequence (2 to_power k)) . i by A21, A56, PARTFUN1:def 6
.= 1 by A58, A66, Th7 ;
A85: ((n -BinarySequence (2 to_power k)) '&' Mbx) . i = ((n -BinarySequence (2 to_power k)) /. i) '&' (Mbx /. i) by A21, A56, Def5
.= (n -BinarySequence (2 to_power k)) /. i by A62 ;
A86: ((n -BinarySequence 0) '&' Mbx) . i = ((n -BinarySequence 0) /. i) '&' (Mbx /. i) by A21, A56, Def5
.= (n -BinarySequence 0) /. i by A62 ;
g in R by A63;
then A87: f | B = g | B by A49, A61, A81;
Absval ((n -BinarySequence 0) '&' (M . bx)) = f . bx by A53
.= (f | B) . bx by A59, FUNCT_1:49
.= g . bx by A59, A87, FUNCT_1:49
.= Absval ((n -BinarySequence (2 to_power k)) '&' (M . bx)) by A63 ;
hence contradiction by A83, A86, A85, A84, BINARI_3:2; :: thesis: verum

end;

hence x in F by A1, A48; :: thesis: verum

end;

hence F = Dependency-str DB-Rel(# X,D,R #) by TARSKI:2; :: thesis: verum

end;

end;