deffunc H1( Nat, Nat, Nat) -> set = (1 * \$1) + (- 1);
A1: for n being Nat
for i1, i2, i3, i4 being Element of n
for a being Integer holds { p where p is b1 -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = a * (p . i4) } is diophantine Subset of () by HILB10_3:6;
defpred S1[ Nat, Nat, Integer] means (1 * \$1) * \$2 = \$3;
A2: for n being Nat
for i1, i2, i3 being Element of n
for a being Integer holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,a * (p . i3)] } is diophantine Subset of () by HILB10_3:9;
A3: for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,H1(p . i3,p . i4,p . i5)] } is diophantine Subset of () from deffunc H2( Nat, Nat, Nat) -> Element of omega = \$1 ! ;
A4: for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H2(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of () by Th32;
defpred S2[ Nat, Nat, natural object , Nat, Nat, Nat] means (1 * \$1) * \$3 = (1 * \$2) - 1;
A5: now :: thesis: for n being Nat
for i1, i3, i2, i4, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S2[p . i1,p . i3,p . i2,p . i4,p . i5,p . i6] } is diophantine Subset of ()
let n be Nat; :: thesis: for i1, i3, i2, i4, i5, i6 being Element of n holds { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i3,p . i2,p . i4,p . i5,p . i6] } is diophantine Subset of ()
let i1, i3, i2, i4, i5, i6 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i3,p . i2,p . i4,p . i5,p . i6] } is diophantine Subset of ()
defpred S3[ XFinSequence of NAT ] means S1[\$1 . i1,\$1 . i2,(1 * (\$1 . i3)) + (- 1)];
defpred S4[ XFinSequence of NAT ] means S2[\$1 . i1,\$1 . i3,\$1 . i2,\$1 . i4,\$1 . i5,\$1 . i6];
A6: for p being n -element XFinSequence of NAT holds
( S3[p] iff S4[p] ) ;
{ p where p is n -element XFinSequence of NAT : S3[p] } = { q where q is n -element XFinSequence of NAT : S4[q] } from hence { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i3,p . i2,p . i4,p . i5,p . i6] } is diophantine Subset of () by A3; :: thesis: verum
end;
A7: for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S2[p . i1,p . i2,H2(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of () from defpred S3[ Nat, Nat, natural object , Nat, Nat, Nat] means (1 * \$3) * (\$1 !) = (1 * \$2) - 1;
A8: for n being Nat
for i1, i4, i2, i3, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S3[p . i1,p . i4,p . i2,p . i3,p . i5,p . i6] } is diophantine Subset of () by A7;
deffunc H3( Nat, Nat, Nat) -> Element of omega = (1 * \$1) + 1;
A9: for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H3(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of () by HILB10_3:15;
A10: for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S3[p . i1,p . i2,H3(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of () from let n be Nat; :: thesis: for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : 1 + (((p . i1) + 1) * ((p . i2) !)) = p . i3 } is diophantine Subset of ()
let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : 1 + (((p . i1) + 1) * ((p . i2) !)) = p . i3 } is diophantine Subset of ()
defpred S4[ XFinSequence of NAT ] means S3[\$1 . i2,\$1 . i3,(1 * (\$1 . i1)) + 1,\$1 . i3,\$1 . i3,\$1 . i3];
defpred S5[ XFinSequence of NAT ] means 1 + (((\$1 . i1) + 1) * ((\$1 . i2) !)) = \$1 . i3;
A11: for p being n -element XFinSequence of NAT holds
( S4[p] iff S5[p] ) ;
{ p where p is n -element XFinSequence of NAT : S4[p] } = { q where q is n -element XFinSequence of NAT : S5[q] } from hence { p where p is n -element XFinSequence of NAT : 1 + (((p . i1) + 1) * ((p . i2) !)) = p . i3 } is diophantine Subset of () by A10; :: thesis: verum