deffunc H₁( Nat, Nat, Nat) -> object = |.F₁($1,$2,$3).|;
defpred S₁[ Nat, Nat, natural object , Nat, Nat, Nat] means ( P₁[$1,$2,1 * $3] & F₁($4,$5,$6) >= 0 );
defpred S₂[ Nat, Nat, natural object , Nat, Nat, Nat] means ( P₁[$1,$2,(- 1) * $3] & F₁($4,$5,$6) <= 0 );
A3: for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)

let n be Nat; :: thesis:
let i1, i2, i3, i4, i5, i6 be Element of n; :: thesis:
set M = { p where p is n -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } ;

suppose A4: n = 0 ; :: thesis:

{ p where p is n -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } c= n -xtuples_of NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is n -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } ; :: thesis:
then ex p being n -element XFinSequence of NAT st
( x = p & S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] ) ;
hence x in n -xtuples_of NAT by HILB10_2:def 5; :: thesis:

end;

hence { p where p is n -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT) by A4; :: thesis:

end;

suppose A5: n <> 0 ; :: thesis:

set n1 = n + 1;
A6: n < n + 1 by NAT_1:13;
then n in Segm (n + 1) by NAT_1:44;
then reconsider I1 = i1, I2 = i2, I3 = i3, I4 = i4, I5 = i5, I6 = i6, N = n as Element of n + 1 by Th2;
defpred S₃[ XFinSequence of NAT ] means P₁[$1 . I1,$1 . I2,1 * ($1 . I3)];
reconsider P = { p where p is n + 1 -element XFinSequence of NAT : S₃[p] } as diophantine Subset of ((n + 1) -xtuples_of NAT) by A1;
reconsider F = { p where p is n + 1 -element XFinSequence of NAT : F₁((p . I4),(p . I5),(p . I6)) = 1 * (p . N) } as diophantine Subset of ((n + 1) -xtuples_of NAT) by A2;
reconsider PF = P /\ F as Subset of ((n + 1) -xtuples_of NAT) ;
reconsider PFk = { (p | n) where p is n + 1 -element XFinSequence of NAT : p in PF } as diophantine Subset of (n -xtuples_of NAT) by Th5, A6;
A7: PFk c= { p where p is n -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in PFk ; :: thesis:
then consider p being n + 1 -element XFinSequence of NAT such that
A8: ( x = p | n & p in PF ) ;
p in P by A8, XBOOLE_0:def 4;
then A9: ex q being n + 1 -element XFinSequence of NAT st
( p = q & S₃[q] ) ;
p in F by A8, XBOOLE_0:def 4;
then A10: ex q being n + 1 -element XFinSequence of NAT st
( p = q & F₁((q . I4),(q . I5),(q . I6)) = 1 * (q . N) ) ;
len p = n + 1 by CARD_1:def 7;
then len (p | n) = n by A6, AFINSQ_1:54;
then reconsider pn = p | n as n -element XFinSequence of NAT by CARD_1:def 7;
( p . I1 = pn . I1 & p . I2 = pn . I2 & p . I3 = pn . I3 & p . I4 = pn . I4 & pn . I5 = p . I5 & pn . i6 = p . I6 ) by A5, Th4;
hence x in { p where p is n -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } by A8, A9, A10; :: thesis:

end;

{ p where p is n -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } c= PFk

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is n -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } ; :: thesis:
then consider p being n -element XFinSequence of NAT such that
A11: ( x = p & S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] ) ;
reconsider FF = F₁((p . i4),(p . i5),(p . i6)) as Element of NAT by A11, INT_1:3;
reconsider Z = <%FF%> as 1 -element XFinSequence of NAT ;
set pZ = p ^ Z;
A12: len p = n by CARD_1:def 7;
then A13: ( (p ^ Z) | n = p & (p ^ Z) . n = FF ) by AFINSQ_1:57, AFINSQ_1:36;
then ( p . i1 = (p ^ Z) . i1 & p . i2 = (p ^ Z) . i2 & p . i3 = (p ^ Z) . i3 & p . i4 = (p ^ Z) . i4 & p . i5 = (p ^ Z) . i5 & p . i6 = (p ^ Z) . i6 ) by A5, Th4;
then ( F₁(((p ^ Z) . i4),((p ^ Z) . i5),((p ^ Z) . i6)) = 1 * ((p ^ Z) . n) & P₁[(p ^ Z) . i1,(p ^ Z) . i2,1 * ((p ^ Z) . i3)] ) by A11, A12, AFINSQ_1:36;
then ( p ^ Z in F & p ^ Z in P ) ;
then p ^ Z in P /\ F by XBOOLE_0:def 4;
hence x in PFk by A13, A11; :: thesis:

end;

hence { p where p is n -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT) by A7, XBOOLE_0:def 10; :: thesis:

end;

A14: for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)

proof

let n be Nat; :: thesis:
let i1, i2, i3, i4, i5, i6 be Element of n; :: thesis:
set M = { p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } ;

per cases ;

suppose A15: n = 0 ; :: thesis:

{ p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } c= n -xtuples_of NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } ; :: thesis:
then ex p being n -element XFinSequence of NAT st
( x = p & S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] ) ;
hence x in n -xtuples_of NAT by HILB10_2:def 5; :: thesis:

end;

hence { p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT) by A15; :: thesis:

end;

suppose A16: n <> 0 ; :: thesis:

set n1 = n + 1;
A17: n < n + 1 by NAT_1:13;
then n in Segm (n + 1) by NAT_1:44;
then reconsider I1 = i1, I2 = i2, I3 = i3, I4 = i4, I5 = i5, I6 = i6, N = n as Element of n + 1 by Th2;
defpred S₃[ XFinSequence of NAT ] means P₁[$1 . I1,$1 . I2,(- 1) * ($1 . I3)];
reconsider P = { p where p is n + 1 -element XFinSequence of NAT : S₃[p] } as diophantine Subset of ((n + 1) -xtuples_of NAT) by A1;
reconsider F = { p where p is n + 1 -element XFinSequence of NAT : F₁((p . I4),(p . I5),(p . I6)) = (- 1) * (p . N) } as diophantine Subset of ((n + 1) -xtuples_of NAT) by A2;
reconsider PF = P /\ F as Subset of ((n + 1) -xtuples_of NAT) ;
reconsider PFk = { (p | n) where p is n + 1 -element XFinSequence of NAT : p in PF } as diophantine Subset of (n -xtuples_of NAT) by Th5, A17;
A18: PFk c= { p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in PFk ; :: thesis:
then consider p being n + 1 -element XFinSequence of NAT such that
A19: ( x = p | n & p in PF ) ;
p in P by A19, XBOOLE_0:def 4;
then A20: ex q being n + 1 -element XFinSequence of NAT st
( p = q & S₃[q] ) ;
p in F by A19, XBOOLE_0:def 4;
then A21: ex q being n + 1 -element XFinSequence of NAT st
( p = q & F₁((q . I4),(q . I5),(q . I6)) = (- 1) * (q . N) ) ;
len p = n + 1 by CARD_1:def 7;
then len (p | n) = n by A17, AFINSQ_1:54;
then reconsider pn = p | n as n -element XFinSequence of NAT by CARD_1:def 7;
( p . I1 = pn . I1 & p . I2 = pn . I2 & p . I3 = pn . I3 & p . I4 = pn . I4 & pn . I5 = p . I5 & pn . i6 = p . I6 ) by A16, Th4;
hence x in { p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } by A19, A20, A21; :: thesis:

end;

{ p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } c= PFk

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } ; :: thesis:
then consider p being n -element XFinSequence of NAT such that
A22: ( x = p & S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] ) ;
reconsider FF = - F₁((p . i4),(p . i5),(p . i6)) as Element of NAT by A22, INT_1:3;
reconsider Z = <%FF%> as 1 -element XFinSequence of NAT ;
set pZ = p ^ Z;
len p = n by CARD_1:def 7;
then A23: ( (p ^ Z) | n = p & (p ^ Z) . n = FF ) by AFINSQ_1:57, AFINSQ_1:36;
then ( p . i1 = (p ^ Z) . i1 & p . i2 = (p ^ Z) . i2 & p . i3 = (p ^ Z) . i3 & p . i4 = (p ^ Z) . i4 & p . i5 = (p ^ Z) . i5 & p . i6 = (p ^ Z) . i6 ) by A16, Th4;
then ( F₁(((p ^ Z) . i4),((p ^ Z) . i5),((p ^ Z) . i6)) = (- 1) * ((p ^ Z) . n) & P₁[(p ^ Z) . i1,(p ^ Z) . i2,(- 1) * ((p ^ Z) . i3)] ) by A22, A23;
then ( p ^ Z in F & p ^ Z in P ) ;
then p ^ Z in P /\ F by XBOOLE_0:def 4;
hence x in PFk by A23, A22; :: thesis:

end;

hence { p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT) by A18, XBOOLE_0:def 10; :: thesis:

end;

A24: for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : H₁(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)

proof

let n be Nat; :: thesis:
let i1, i2, i3, i4 be Element of n; :: thesis:
defpred S₃[ XFinSequence of NAT ] means F₁(($1 . i1),($1 . i2),($1 . i3)) = 1 * ($1 . i4);
defpred S₄[ XFinSequence of NAT ] means F₁(($1 . i1),($1 . i2),($1 . i3)) = (- 1) * ($1 . i4);
A25: { p where p is n -element XFinSequence of NAT : S₃[p] } is diophantine Subset of (n -xtuples_of NAT) by A2;
A26: { p where p is n -element XFinSequence of NAT : S₄[p] } is diophantine Subset of (n -xtuples_of NAT) by A2;
A27: { p where p is n -element XFinSequence of NAT : ( S₃[p] or S₄[p] ) } is diophantine Subset of (n -xtuples_of NAT) from HILB10_3:sch 1(A25, A26);
defpred S₅[ XFinSequence of NAT ] means ( S₃[$1] or S₄[$1] );
defpred S₆[ XFinSequence of NAT ] means H₁($1 . i1,$1 . i2,$1 . i3) = $1 . i4;
A28: for p being n -element XFinSequence of NAT holds
( S₅[p] iff S₆[p] )

proof

let p be n -element XFinSequence of NAT ; :: thesis:
thus ( S₅[p] implies S₆[p] ) :: thesis:

proof

assume A29: S₅[p] ; :: thesis:

per cases by A29;

suppose S₃[p] ; :: thesis:

hence S₆[p] by ABSVALUE:def 1; :: thesis:

end;

suppose S₄[p] ; :: thesis:

then H₁(p . i1,p . i2,p . i3) = - ((- 1) * (p . i4)) by ABSVALUE:30;
hence S₆[p] ; :: thesis:

end;

assume A30: S₆[p] ; :: thesis:

per cases ),(p . i2),(p . i3)) >= 0 or F₁((p . i1),(p . i2),(p . i3)) < 0 ) ;

suppose F₁((p . i1),(p . i2),(p . i3)) >= 0 ; :: thesis:

hence S₅[p] by A30, ABSVALUE:def 1; :: thesis:

end;

suppose F₁((p . i1),(p . i2),(p . i3)) < 0 ; :: thesis:

then H₁(p . i1,p . i2,p . i3) = - F₁((p . i1),(p . i2),(p . i3)) by ABSVALUE:def 1;
hence S₅[p] by A30; :: thesis:

end;

{ p where p is n -element XFinSequence of NAT : S₅[p] } = { q where q is n -element XFinSequence of NAT : S₆[q] } from HILB10_3:sch 2(A28);
hence { p where p is n -element XFinSequence of NAT : H₁(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT) by A27; :: thesis:

end;

A31: for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : S₁[p . i1,p . i2,H₁(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT) from HILB10_3:sch 4(A3, A24);
A32: for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : S₂[p . i1,p . i2,H₁(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT) from HILB10_3:sch 4(A14, A24);
let n be Nat; :: thesis:
let i1, i2, i3, i4, i5 be Element of n; :: thesis:
defpred S₃[ XFinSequence of NAT ] means S₁[$1 . i1,$1 . i2,H₁($1 . i3,$1 . i4,$1 . i5),$1 . i3,$1 . i4,$1 . i5];
defpred S₄[ XFinSequence of NAT ] means S₂[$1 . i1,$1 . i2,H₁($1 . i3,$1 . i4,$1 . i5),$1 . i3,$1 . i4,$1 . i5];
defpred S₅[ XFinSequence of NAT ] means ( S₃[$1] or S₄[$1] );
A33: { p where p is n -element XFinSequence of NAT : S₃[p] } is diophantine Subset of (n -xtuples_of NAT) by A31;
A34: { p where p is n -element XFinSequence of NAT : S₄[p] } is diophantine Subset of (n -xtuples_of NAT) by A32;
A35: { p where p is n -element XFinSequence of NAT : ( S₃[p] or S₄[p] ) } is diophantine Subset of (n -xtuples_of NAT) from HILB10_3:sch 1(A33, A34);
defpred S₆[ XFinSequence of NAT ] means P₁[$1 . i1,$1 . i2,F₁(($1 . i3),($1 . i4),($1 . i5))];
A36: for p being n -element XFinSequence of NAT holds
( S₅[p] iff S₆[p] )

proof

let p be n -element XFinSequence of NAT ; :: thesis:
thus ( S₅[p] implies S₆[p] ) :: thesis:

proof

assume A37: ( S₃[p] or S₄[p] ) ; :: thesis:

per cases by A37;

suppose S₃[p] ; :: thesis:

hence S₆[p] by ABSVALUE:def 1; :: thesis:

end;

suppose A38: S₄[p] ; :: thesis:

then H₁(p . i3,p . i4,p . i5) = - F₁((p . i3),(p . i4),(p . i5)) by ABSVALUE:30;
hence S₆[p] by A38; :: thesis:

end;

assume A39: S₆[p] ; :: thesis:

per cases ),(p . i4),(p . i5)) >= 0 or F₁((p . i3),(p . i4),(p . i5)) < 0 ) ;

suppose F₁((p . i3),(p . i4),(p . i5)) >= 0 ; :: thesis:

hence S₅[p] by A39, ABSVALUE:def 1; :: thesis:

end;

suppose A40: F₁((p . i3),(p . i4),(p . i5)) < 0 ; :: thesis:

then H₁(p . i3,p . i4,p . i5) = - F₁((p . i3),(p . i4),(p . i5)) by ABSVALUE:def 1;
hence S₅[p] by A39, A40; :: thesis:

end;

{ p where p is n -element XFinSequence of NAT : S₅[p] } = { q where q is n -element XFinSequence of NAT : S₆[q] } from HILB10_3:sch 2(A36);
hence { p where p is n -element XFinSequence of NAT : P₁[p . i1,p . i2,F₁((p . i3),(p . i4),(p . i5))] } is diophantine Subset of (n -xtuples_of NAT) by A35; :: thesis: