deffunc H1( Nat, Nat, Nat) -> Element of omega = \$1 ! ;
A1: for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of () by Th32;
defpred S1[ Nat, Nat, natural object , Nat, Nat, Nat] means ( \$1 = Product (1 + (\$3 * (idseq \$2))) & \$3 >= 1 );
A2: for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of () by Th35;
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),p . i3,p . i4,p . i5] } is diophantine Subset of () from deffunc H2( Nat, Nat, Nat) -> Element of omega = (1 * \$1) + 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 HILB10_3:15;
defpred S2[ Nat, Nat, natural object , Nat, Nat, Nat] means ( \$1 = Product (1 + ((\$2 !) * (idseq \$3))) & \$2 ! >= 1 );
A5: 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 () by A3;
A6: 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 let n be Nat; :: thesis: for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i3 = Product (1 + (((p . i1) !) * (idseq (1 + (p . i2))))) } is diophantine Subset of ()
let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i3 = Product (1 + (((p . i1) !) * (idseq (1 + (p . i2))))) } is diophantine Subset of ()
defpred S3[ XFinSequence of NAT ] means S2[\$1 . i3,\$1 . i1,(1 * (\$1 . i2)) + 1,1 * (\$1 . i3),\$1 . i3,\$1 . i3];
defpred S4[ XFinSequence of NAT ] means \$1 . i3 = Product (1 + (((\$1 . i1) !) * (idseq (1 + (\$1 . i2)))));
A7: for p being n -element XFinSequence of NAT holds
( S3[p] iff S4[p] ) by NAT_1:14;
{ 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 : p . i3 = Product (1 + (((p . i1) !) * (idseq (1 + (p . i2))))) } is diophantine Subset of () by A6; :: thesis: verum