:: by Karol P\kak

::

:: Received March 27, 2018

:: Copyright (c) 2018 Association of Mizar Users

registration

let X be non empty set ;

let n be Nat;

ex b_{1} being XFinSequence of X st b_{1} is n -element

end;
let n be Nat;

cluster Relation-like omega -defined X -valued Function-like Sequence-like finite n -element finite-support V268() for XFinSequence of ;

existence ex b

proof end;

registration

let n be Nat;

ex b_{1} being XFinSequence st

( b_{1} is n -element & b_{1} is real-valued )

end;
cluster Relation-like omega -defined Function-like Sequence-like finite n -element real-valued finite-support V268() for XFinSequence;

existence ex b

( b

proof end;

registration

let n, m be Nat;

let p be n -element XFinSequence;

let q be m -element XFinSequence;

coherence

p ^ q is n + m -element

end;
let p be n -element XFinSequence;

let q be m -element XFinSequence;

coherence

p ^ q is n + m -element

proof end;

definition

let n be Nat;

let p be n -element real-valued XFinSequence;

coherence

p is Function of n,F_Real

end;
let p be n -element real-valued XFinSequence;

coherence

p is Function of n,F_Real

proof end;

:: deftheorem defines @ HILB10_2:def 1 :

for n being Nat

for p being b_{1} -element real-valued XFinSequence holds @ p = p;

for n being Nat

for p being b

definition

let n be Nat;

let X be non empty set ;

let p be Function of n,X;

coherence

p is n -element XFinSequence of X

end;
let X be non empty set ;

let p be Function of n,X;

coherence

p is n -element XFinSequence of X

proof end;

:: deftheorem defines @ HILB10_2:def 2 :

for n being Nat

for X being non empty set

for p being Function of n,X holds @ p = p;

for n being Nat

for X being non empty set

for p being Function of n,X holds @ p = p;

registration

let X be set ;

let p be Permutation of X;

let M be ManySortedSet of X;

coherence

M * p is total

end;
let p be Permutation of X;

let M be ManySortedSet of X;

coherence

M * p is total

proof end;

registration

let F be finite-support Function;

let f be one-to-one Function;

coherence

F * f is finite-support

end;
let f be one-to-one Function;

coherence

F * f is finite-support

proof end;

theorem Th2: :: HILB10_2:2

for X being set

for f being b_{1} -defined Function

for perm being Permutation of X holds card (support (f * perm)) = card (support f)

for f being b

for perm being Permutation of X holds card (support (f * perm)) = card (support f)

proof end;

registration

let X be set ;

coherence

0_ (X,F_Real) is natural-valued

1_ (X,F_Real) is natural-valued

end;
coherence

0_ (X,F_Real) is natural-valued

proof end;

coherence 1_ (X,F_Real) is natural-valued

proof end;

registration
end;

registration

let X be set ;

ex b_{1} being Series of X,F_Real st b_{1} is INT -valued

end;
cluster Relation-like Bags X -defined INT -valued the carrier of F_Real -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued for Series of ,;

existence ex b

proof end;

registration

let O be Ordinal;

ex b_{1} being Polynomial of O,F_Real st b_{1} is INT -valued

end;
cluster Relation-like Bags O -defined INT -valued the carrier of F_Real -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued finite-Support for Polynomial of ,;

existence ex b

proof end;

registration

let X be set ;

let p be INT -valued Series of X,F_Real;

coherence

- p is INT -valued

coherence

p + q is INT -valued

p - q is INT -valued

end;
let p be INT -valued Series of X,F_Real;

coherence

- p is INT -valued

proof end;

let q be INT -valued Series of X,F_Real;coherence

p + q is INT -valued

proof end;

coherence p - q is INT -valued

proof end;

registration

let X be Ordinal;

let p, q be INT -valued Series of X,F_Real;

coherence

p *' q is INT -valued

end;
let p, q be INT -valued Series of X,F_Real;

coherence

p *' q is INT -valued

proof end;

registration

let X be set ;

ex b_{1} being Function of X,F_Real st b_{1} is natural-valued

end;
cluster Relation-like X -defined the carrier of F_Real -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued for Function of ,;

existence ex b

proof end;

registration

let O be Ordinal;

ex b_{1} being Function of O,F_Real st b_{1} is INT -valued

end;
cluster Relation-like O -defined INT -valued the carrier of F_Real -valued Function-like total quasi_total complex-valued ext-real-valued real-valued for Function of ,;

existence ex b

proof end;

registration

let O be Ordinal;

let b be bag of O;

let x be INT -valued Function of O,F_Real;

coherence

eval (b,x) is integer

end;
let b be bag of O;

let x be INT -valued Function of O,F_Real;

coherence

eval (b,x) is integer

proof end;

registration

let O be Ordinal;

let p be INT -valued Polynomial of O,F_Real;

let x be INT -valued Function of O,F_Real;

coherence

eval (p,x) is integer

end;
let p be INT -valued Polynomial of O,F_Real;

let x be INT -valued Function of O,F_Real;

coherence

eval (p,x) is integer

proof end;

definition

let n be Nat;

let L be non empty ZeroStr ;

let p be Series of n,L;

ex b_{1} being Series of (n + 1),L st

for b being bag of n + 1 holds

( ( b . n <> 0 implies b_{1} . b = 0. L ) & ( b . n = 0 implies b_{1} . b = p . ((0,n) -cut b) ) )

for b_{1}, b_{2} being Series of (n + 1),L st ( for b being bag of n + 1 holds

( ( b . n <> 0 implies b_{1} . b = 0. L ) & ( b . n = 0 implies b_{1} . b = p . ((0,n) -cut b) ) ) ) & ( for b being bag of n + 1 holds

( ( b . n <> 0 implies b_{2} . b = 0. L ) & ( b . n = 0 implies b_{2} . b = p . ((0,n) -cut b) ) ) ) holds

b_{1} = b_{2}

end;
let L be non empty ZeroStr ;

let p be Series of n,L;

func p extended_by_0 -> Series of (n + 1),L means :Def3: :: HILB10_2:def 3

for b being bag of n + 1 holds

( ( b . n <> 0 implies it . b = 0. L ) & ( b . n = 0 implies it . b = p . ((0,n) -cut b) ) );

existence for b being bag of n + 1 holds

( ( b . n <> 0 implies it . b = 0. L ) & ( b . n = 0 implies it . b = p . ((0,n) -cut b) ) );

ex b

for b being bag of n + 1 holds

( ( b . n <> 0 implies b

proof end;

uniqueness for b

( ( b . n <> 0 implies b

( ( b . n <> 0 implies b

b

proof end;

:: deftheorem Def3 defines extended_by_0 HILB10_2:def 3 :

for n being Nat

for L being non empty ZeroStr

for p being Series of n,L

for b_{4} being Series of (n + 1),L holds

( b_{4} = p extended_by_0 iff for b being bag of n + 1 holds

( ( b . n <> 0 implies b_{4} . b = 0. L ) & ( b . n = 0 implies b_{4} . b = p . ((0,n) -cut b) ) ) );

for n being Nat

for L being non empty ZeroStr

for p being Series of n,L

for b

( b

( ( b . n <> 0 implies b

theorem Th6: :: HILB10_2:6

for n being Nat

for b being bag of n

for L being non empty ZeroStr

for p being Series of n,L holds (p extended_by_0) . (b bag_extend 0) = p . b

for b being bag of n

for L being non empty ZeroStr

for p being Series of n,L holds (p extended_by_0) . (b bag_extend 0) = p . b

proof end;

theorem Th7: :: HILB10_2:7

for n being Nat

for L being non empty ZeroStr

for p being Series of n,L

for b being bag of n + 1 st b in Support (p extended_by_0) holds

b . n = 0

for L being non empty ZeroStr

for p being Series of n,L

for b being bag of n + 1 st b in Support (p extended_by_0) holds

b . n = 0

proof end;

theorem Th8: :: HILB10_2:8

for n being Nat

for b being bag of n

for L being non empty ZeroStr

for p being Series of n,L holds

( b bag_extend 0 in Support (p extended_by_0) iff b in Support p )

for b being bag of n

for L being non empty ZeroStr

for p being Series of n,L holds

( b bag_extend 0 in Support (p extended_by_0) iff b in Support p )

proof end;

theorem Th9: :: HILB10_2:9

for n being Nat

for L being non empty ZeroStr

for p being Series of n,L

for b being bag of n + 1 st b . n = 0 holds

( b in Support (p extended_by_0) iff (0,n) -cut b in Support p )

for L being non empty ZeroStr

for p being Series of n,L

for b being bag of n + 1 st b . n = 0 holds

( b in Support (p extended_by_0) iff (0,n) -cut b in Support p )

proof end;

registration

let n be Nat;

let L be non empty ZeroStr ;

let p be Polynomial of n,L;

coherence

p extended_by_0 is finite-Support

end;
let L be non empty ZeroStr ;

let p be Polynomial of n,L;

coherence

p extended_by_0 is finite-Support

proof end;

theorem Th10: :: HILB10_2:10

for n being Nat

for L being non empty ZeroStr

for p being Series of n,L holds {(0. L)} \/ (rng p) = rng (p extended_by_0)

for L being non empty ZeroStr

for p being Series of n,L holds {(0. L)} \/ (rng p) = rng (p extended_by_0)

proof end;

theorem Th12: :: HILB10_2:12

for n being Nat

for b being bag of n holds SgmX ((RelIncl n),(support b)) = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))

for b being bag of n holds SgmX ((RelIncl n),(support b)) = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))

proof end;

theorem Th13: :: HILB10_2:13

for n being Nat

for b being bag of n

for L being non trivial well-unital doubleLoopStr

for x being Function of n,L

for y being Function of (n + 1),L st y | n = x holds

eval (b,x) = eval ((b bag_extend 0),y)

for b being bag of n

for L being non trivial well-unital doubleLoopStr

for x being Function of n,L

for y being Function of (n + 1),L st y | n = x holds

eval (b,x) = eval ((b bag_extend 0),y)

proof end;

theorem Th14: :: HILB10_2:14

for k, n being Nat

for b1, b2 being bag of n holds

( b1 < b2 iff b1 bag_extend k < b2 bag_extend k )

for b1, b2 being bag of n holds

( b1 < b2 iff b1 bag_extend k < b2 bag_extend k )

proof end;

theorem :: HILB10_2:15

for X being non empty set

for A being finite Subset of X

for R being Order of X st R linearly_orders A holds

for i, k being Nat st 1 <= i & i <= k & k <= card A holds

(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,A)) /. i

for A being finite Subset of X

for R being Order of X st R linearly_orders A holds

for i, k being Nat st 1 <= i & i <= k & k <= card A holds

(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,A)) /. i

proof end;

theorem Th16: :: HILB10_2:16

for n, m being Nat

for O being Ordinal

for A being finite Subset of (Bags O) st n in dom (SgmX ((BagOrder O),A)) & m in dom (SgmX ((BagOrder O),A)) & n < m holds

(SgmX ((BagOrder O),A)) /. n < (SgmX ((BagOrder O),A)) /. m

for O being Ordinal

for A being finite Subset of (Bags O) st n in dom (SgmX ((BagOrder O),A)) & m in dom (SgmX ((BagOrder O),A)) & n < m holds

(SgmX ((BagOrder O),A)) /. n < (SgmX ((BagOrder O),A)) /. m

proof end;

theorem Th17: :: HILB10_2:17

for n being Nat

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L holds

( len (SgmX ((BagOrder n),(Support p))) = len (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) & ( for i being Nat st 1 <= i & i <= len (SgmX ((BagOrder n),(Support p))) holds

(SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 ) )

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L holds

( len (SgmX ((BagOrder n),(Support p))) = len (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) & ( for i being Nat st 1 <= i & i <= len (SgmX ((BagOrder n),(Support p))) holds

(SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 ) )

proof end;

theorem Th18: :: HILB10_2:18

for n being Nat

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L

for x being Function of n,L

for y being Function of (n + 1),L st y | n = x holds

eval (p,x) = eval ((p extended_by_0),y)

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L

for x being Function of n,L

for y being Function of (n + 1),L st y | n = x holds

eval (p,x) = eval ((p extended_by_0),y)

proof end;

theorem Th19: :: HILB10_2:19

for O being Ordinal

for L being non trivial associative commutative well-unital doubleLoopStr

for x being Function of O,L

for b being bag of O

for S being one-to-one FinSequence of O st rng S = support b holds

ex y being FinSequence of L st

( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds

y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )

for L being non trivial associative commutative well-unital doubleLoopStr

for x being Function of O,L

for b being bag of O

for S being one-to-one FinSequence of O st rng S = support b holds

ex y being FinSequence of L st

( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds

y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )

proof end;

theorem Th20: :: HILB10_2:20

for O being Ordinal

for L being non trivial associative commutative well-unital doubleLoopStr

for x being Function of O,L

for b being bag of O

for perm being Permutation of O holds eval (b,x) = eval ((b * perm),(x * perm))

for L being non trivial associative commutative well-unital doubleLoopStr

for x being Function of O,L

for b being bag of O

for perm being Permutation of O holds eval (b,x) = eval ((b * perm),(x * perm))

proof end;

definition

let O be Ordinal;

let L be non empty ZeroStr ;

let s be Series of O,L;

let perm be Permutation of O;

ex b_{1} being Series of O,L st

for b being bag of O holds b_{1} . b = s . (b * perm)

for b_{1}, b_{2} being Series of O,L st ( for b being bag of O holds b_{1} . b = s . (b * perm) ) & ( for b being bag of O holds b_{2} . b = s . (b * perm) ) holds

b_{1} = b_{2}

end;
let L be non empty ZeroStr ;

let s be Series of O,L;

let perm be Permutation of O;

func s permuted_by perm -> Series of O,L means :Def4: :: HILB10_2:def 4

for b being bag of O holds it . b = s . (b * perm);

existence for b being bag of O holds it . b = s . (b * perm);

ex b

for b being bag of O holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines permuted_by HILB10_2:def 4 :

for O being Ordinal

for L being non empty ZeroStr

for s being Series of O,L

for perm being Permutation of O

for b_{5} being Series of O,L holds

( b_{5} = s permuted_by perm iff for b being bag of O holds b_{5} . b = s . (b * perm) );

for O being Ordinal

for L being non empty ZeroStr

for s being Series of O,L

for perm being Permutation of O

for b

( b

theorem Th21: :: HILB10_2:21

for O being Ordinal

for L being non empty ZeroStr

for perm being Permutation of O

for s being Series of O,L

for b being bag of O holds

( b in Support (s permuted_by perm) iff b * perm in Support s )

for L being non empty ZeroStr

for perm being Permutation of O

for s being Series of O,L

for b being bag of O holds

( b in Support (s permuted_by perm) iff b * perm in Support s )

proof end;

theorem Th22: :: HILB10_2:22

for O being Ordinal

for L being non empty ZeroStr

for perm being Permutation of O

for s being Series of O,L

for b being bag of O holds

( b * (perm ") in Support (s permuted_by perm) iff b in Support s )

for L being non empty ZeroStr

for perm being Permutation of O

for s being Series of O,L

for b being bag of O holds

( b * (perm ") in Support (s permuted_by perm) iff b in Support s )

proof end;

theorem Th23: :: HILB10_2:23

for O being Ordinal

for L being non empty ZeroStr

for perm being Permutation of O

for s being Series of O,L holds card (Support s) = card (Support (s permuted_by perm))

for L being non empty ZeroStr

for perm being Permutation of O

for s being Series of O,L holds card (Support s) = card (Support (s permuted_by perm))

proof end;

theorem Th24: :: HILB10_2:24

for O being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of O,L

for x being Function of O,L

for S being one-to-one FinSequence of Bags O st rng S = Support p holds

ex y being FinSequence of L st

( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds

y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of O,L

for x being Function of O,L

for S being one-to-one FinSequence of Bags O st rng S = Support p holds

ex y being FinSequence of L st

( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds

y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )

proof end;

registration

let O be Ordinal;

let L be non empty ZeroStr ;

let perm be Permutation of O;

let p be Polynomial of O,L;

coherence

p permuted_by perm is finite-Support

end;
let L be non empty ZeroStr ;

let perm be Permutation of O;

let p be Polynomial of O,L;

coherence

p permuted_by perm is finite-Support

proof end;

theorem Th25: :: HILB10_2:25

for O being Ordinal

for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of O,L

for x being Function of O,L

for perm being Permutation of O holds eval (p,x) = eval ((p permuted_by perm),(x * (perm ")))

for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of O,L

for x being Function of O,L

for perm being Permutation of O holds eval (p,x) = eval ((p permuted_by perm),(x * (perm ")))

proof end;

theorem Th26: :: HILB10_2:26

for O being Ordinal

for L being non empty ZeroStr

for s being Series of O,L

for perm being Permutation of O holds rng (s permuted_by perm) = rng s

for L being non empty ZeroStr

for s being Series of O,L

for perm being Permutation of O holds rng (s permuted_by perm) = rng s

proof end;

theorem Th27: :: HILB10_2:27

for n, m being Nat

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L ex q being Polynomial of (n + m),L st

( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L

for y being Function of (n + m),L st y | n = x holds

eval (p,x) = eval (q,y) ) )

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L ex q being Polynomial of (n + m),L st

( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L

for y being Function of (n + m),L st y | n = x holds

eval (p,x) = eval (q,y) ) )

proof end;

theorem Th28: :: HILB10_2:28

for k, n, m being Nat

for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of (n + m),L ex q being Polynomial of ((n + k) + m),L st

( rng q c= (rng p) \/ {(0. L)} & ( for XY being Function of (n + m),L

for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds

eval (p,XY) = eval (q,XanyY) ) )

for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of (n + m),L ex q being Polynomial of ((n + k) + m),L st

( rng q c= (rng p) \/ {(0. L)} & ( for XY being Function of (n + m),L

for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds

eval (p,XY) = eval (q,XanyY) ) )

proof end;

definition

let D be non empty set ;

let n be Nat;

ex b_{1} being Subset of (D ^omega) st

for x being object holds

( x in b_{1} iff x is n -element XFinSequence of D )

for b_{1}, b_{2} being Subset of (D ^omega) st ( for x being object holds

( x in b_{1} iff x is n -element XFinSequence of D ) ) & ( for x being object holds

( x in b_{2} iff x is n -element XFinSequence of D ) ) holds

b_{1} = b_{2}

end;
let n be Nat;

func n -xtuples_of D -> Subset of (D ^omega) means :Def5: :: HILB10_2:def 5

for x being object holds

( x in it iff x is n -element XFinSequence of D );

existence for x being object holds

( x in it iff x is n -element XFinSequence of D );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def5 defines -xtuples_of HILB10_2:def 5 :

for D being non empty set

for n being Nat

for b_{3} being Subset of (D ^omega) holds

( b_{3} = n -xtuples_of D iff for x being object holds

( x in b_{3} iff x is b_{2} -element XFinSequence of D ) );

for D being non empty set

for n being Nat

for b

( b

( x in b

registration

let D be non empty set ;

let n be Nat;

coherence

not n -xtuples_of D is empty

for b_{1} being Element of n -xtuples_of D holds

( b_{1} is n -element & b_{1} is D -valued )
by Def5;

end;
let n be Nat;

coherence

not n -xtuples_of D is empty

proof end;

coherence for b

( b

definition

let n be Nat;

let A be Subset of (n -xtuples_of NAT);

end;
let A be Subset of (n -xtuples_of NAT);

attr A is diophantine means :Def6: :: HILB10_2:def 6

ex m being Nat ex p being INT -valued Polynomial of (n + m),F_Real st

for s being object holds

( s in A iff ex x being n -element XFinSequence of NAT ex y being b_{1} -element XFinSequence of NAT st

( s = x & eval (p,(@ (x ^ y))) = 0 ) );

ex m being Nat ex p being INT -valued Polynomial of (n + m),F_Real st

for s being object holds

( s in A iff ex x being n -element XFinSequence of NAT ex y being b

( s = x & eval (p,(@ (x ^ y))) = 0 ) );

:: deftheorem Def6 defines diophantine HILB10_2:def 6 :

for n being Nat

for A being Subset of (n -xtuples_of NAT) holds

( A is diophantine iff ex m being Nat ex p being INT -valued Polynomial of (n + m),F_Real st

for s being object holds

( s in A iff ex x being b_{1} -element XFinSequence of NAT ex y being b_{3} -element XFinSequence of NAT st

( s = x & eval (p,(@ (x ^ y))) = 0 ) ) );

for n being Nat

for A being Subset of (n -xtuples_of NAT) holds

( A is diophantine iff ex m being Nat ex p being INT -valued Polynomial of (n + m),F_Real st

for s being object holds

( s in A iff ex x being b

( s = x & eval (p,(@ (x ^ y))) = 0 ) ) );

registration

let n be Nat;

coherence

for b_{1} being Subset of (n -xtuples_of NAT) st b_{1} is empty holds

b_{1} is diophantine

[#] (n -xtuples_of NAT) is diophantine

end;
coherence

for b

b

proof end;

coherence [#] (n -xtuples_of NAT) is diophantine

proof end;

registration

let n be zero Nat;

coherence

for b_{1} being Subset of (n -xtuples_of NAT) holds b_{1} is diophantine

end;
coherence

for b

proof end;

registration

let n be Nat;

existence

ex b_{1} being Subset of (n -xtuples_of NAT) st

( not b_{1} is empty & b_{1} is diophantine )

ex b_{1} being Subset of (n -xtuples_of NAT) st

( b_{1} is empty & b_{1} is diophantine )

end;
existence

ex b

( not b

proof end;

existence ex b

( b

proof end;

registration

let n be Nat;

let A, B be diophantine Subset of (n -xtuples_of NAT);

coherence

for b_{1} being Subset of (n -xtuples_of NAT) st b_{1} = A /\ B holds

b_{1} is diophantine

for b_{1} being Subset of (n -xtuples_of NAT) st b_{1} = A \/ B holds

b_{1} is diophantine

end;
let A, B be diophantine Subset of (n -xtuples_of NAT);

coherence

for b

b

proof end;

coherence for b

b

proof end;