reconsider S = F2() as finite set by A2;
defpred S1[ Nat] means for X being finite set st X c= S & card X = \$1 holds
for i2, i3, i4 being Element of F1() holds { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
is diophantine Subset of (F1() -xtuples_of NAT);
A3: S1[ 0 ]
proof
let X be finite set ; :: thesis: ( X c= S & card X = 0 implies for i2, i3, i4 being Element of F1() holds { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
is diophantine Subset of (F1() -xtuples_of NAT) )

assume A4: ( X c= S & card X = 0 ) ; :: thesis: for i2, i3, i4 being Element of F1() holds { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
is diophantine Subset of (F1() -xtuples_of NAT)

let i2, i3, i4 be Element of F1(); :: thesis: { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
is diophantine Subset of (F1() -xtuples_of NAT)

set PP = { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
;
A5: { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4] } c= [#] (F1() -xtuples_of NAT)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
or x in [#] (F1() -xtuples_of NAT) )

assume x in { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
; :: thesis: x in [#] (F1() -xtuples_of NAT)
then ex p being F1() -element XFinSequence of NAT st
( x = p & ( for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4] ) ) ;
hence x in [#] (F1() -xtuples_of NAT) by HILB10_2:def 5; :: thesis: verum
end;
[#] (F1() -xtuples_of NAT) c= { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (F1() -xtuples_of NAT) or x in { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
)

assume x in [#] (F1() -xtuples_of NAT) ; :: thesis: x in { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}

then reconsider p = x as F1() -element XFinSequence of NAT ;
X = {} by A4;
then for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4] by XBOOLE_0:def 1;
hence x in { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
; :: thesis: verum
end;
hence { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F1() -xtuples_of NAT) by ; :: thesis: verum
end;
A6: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A7: S1[m] ; :: thesis: S1[m + 1]
let X be finite set ; :: thesis: ( X c= S & card X = m + 1 implies for i2, i3, i4 being Element of F1() holds { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
is diophantine Subset of (F1() -xtuples_of NAT) )

assume A8: ( X c= S & card X = m + 1 ) ; :: thesis: for i2, i3, i4 being Element of F1() holds { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
is diophantine Subset of (F1() -xtuples_of NAT)

let i2, i3, i4 be Element of F1(); :: thesis: { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4]
}
is diophantine Subset of (F1() -xtuples_of NAT)

not X is empty by A8;
then consider x being object such that
A9: x in X by XBOOLE_0:def 1;
x in S by A8, A9;
then reconsider x = x as Element of F1() by A2;
defpred S2[ XFinSequence of NAT ] means for i being Nat st i in X \ {x} holds
P1[\$1 . i,\$1 . i2,\$1 . i3,\$1 . i4];
card (X \ {x}) = m by ;
then A10: { p where p is F1() -element XFinSequence of NAT : S2[p] } is diophantine Subset of (F1() -xtuples_of NAT) by ;
defpred S3[ XFinSequence of NAT ] means P1[\$1 . x,\$1 . i2,\$1 . i3,\$1 . i4];
A11: { p where p is F1() -element XFinSequence of NAT : S3[p] } is diophantine Subset of (F1() -xtuples_of NAT) by A1;
defpred S4[ XFinSequence of NAT ] means ( S2[\$1] & S3[\$1] );
A12: { p where p is F1() -element XFinSequence of NAT : ( S2[p] & S3[p] ) } is diophantine Subset of (F1() -xtuples_of NAT) from defpred S5[ XFinSequence of NAT ] means for i being Nat st i in X holds
P1[\$1 . i,\$1 . i2,\$1 . i3,\$1 . i4];
A13: for p being F1() -element XFinSequence of NAT holds
( S4[p] iff S5[p] )
proof
let p be F1() -element XFinSequence of NAT ; :: thesis: ( S4[p] iff S5[p] )
thus ( S4[p] implies S5[p] ) :: thesis: ( S5[p] implies S4[p] )
proof
assume A14: S4[p] ; :: thesis: S5[p]
let i be Nat; :: thesis: ( i in X implies P1[p . i,p . i2,p . i3,p . i4] )
assume A15: i in X ; :: thesis: P1[p . i,p . i2,p . i3,p . i4]
( i = x or not i in {x} ) by TARSKI:def 1;
then ( i = x or i in X \ {x} ) by ;
hence P1[p . i,p . i2,p . i3,p . i4] by A14; :: thesis: verum
end;
assume S5[p] ; :: thesis: S4[p]
hence S4[p] by A9, A2; :: thesis: verum
end;
{ p where p is F1() -element XFinSequence of NAT : S4[p] } = { p where p is F1() -element XFinSequence of NAT : S5[p] } from hence { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in X holds
P1[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F1() -xtuples_of NAT) by A12; :: thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch 2(A3, A6);
then S1[ card S] ;
hence for i2, i3, i4 being Element of F1() holds { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in F2() holds
P1[p . i,p . i2,p . i3,p . i4]
}
is diophantine Subset of (F1() -xtuples_of NAT) ; :: thesis: verum