let n be Nat; :: thesis: for i, j being Element of n holds { p where p is n -element XFinSequence of NAT : p . i = (((p . j) -' 1) !) + 1 } is diophantine Subset of ()
A1: for n being Nat
for i1, i2 being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i1 = (p . i2) -' 1 } is diophantine Subset of ()
proof
let n be Nat; :: thesis: for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) -' 1 } is diophantine Subset of ()
let i1, i2 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) -' 1 } is diophantine Subset of ()
defpred S1[ XFinSequence of NAT ] means 1 * (\$1 . i1) = (1 * (\$1 . i2)) -' 1;
defpred S2[ XFinSequence of NAT ] means \$1 . i1 = (\$1 . i2) -' 1;
A2: for q being n -element XFinSequence of NAT holds
( S1[q] iff S2[q] ) ;
{ q where q is n -element XFinSequence of NAT : S1[q] } = { r where r is n -element XFinSequence of NAT : S2[r] } from hence { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) -' 1 } is diophantine Subset of () by HILB10_3:20; :: thesis: verum
end;
A3: for n being Nat
for i1, i2 being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i1 = ((p . i2) -' 1) ! } is diophantine Subset of ()
proof
defpred S1[ Nat, Nat, natural object , Nat, Nat, Nat] means \$4 = \$3 ! ;
deffunc H1( Nat, Nat, Nat) -> Element of omega = \$2 -' 1;
A4: 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 HILB10_4:32;
A5: 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 A1;
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 hence for n being Nat
for i1, i2 being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i1 = ((p . i2) -' 1) ! } is diophantine Subset of () ; :: thesis: verum
end;
defpred S1[ Nat, Nat, natural object , Nat, Nat, Nat] means \$4 = (1 * \$3) + 1;
deffunc H1( Nat, Nat, Nat) -> Element of omega = (\$2 -' 1) ! ;
A6: 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 HILB10_3:15;
A7: 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 A3;
A8: 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 let i1, i2 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = (((p . i2) -' 1) !) + 1 } is diophantine Subset of ()
defpred S2[ XFinSequence of NAT ] means \$1 . i1 = (1 * (((\$1 . i2) -' 1) !)) + 1;
defpred S3[ XFinSequence of NAT ] means \$1 . i1 = (((\$1 . i2) -' 1) !) + 1;
A9: for q being n -element XFinSequence of NAT holds
( S2[q] iff S3[q] ) ;
{ q where q is n -element XFinSequence of NAT : S2[q] } = { r where r is n -element XFinSequence of NAT : S3[r] } from hence { p where p is n -element XFinSequence of NAT : p . i1 = (((p . i2) -' 1) !) + 1 } is diophantine Subset of () by A8; :: thesis: verum