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 A5, XBOOLE_0:def 10; :: 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 A8, A9, STIRL2_1:55;
then A10: { p where p is F1() -element XFinSequence of NAT : S2[p] } is diophantine Subset of (F1() -xtuples_of NAT) by A8, XBOOLE_1:1, A7;
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 HILB10_3:sch 3(A10, A11);
 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 A15, XBOOLE_0:def 5;
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 HILB10_3:sch 2(A13);
 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