reconsider S = F_{2}() as finite set by A2;

defpred S_{1}[ Nat] means for X being finite set st X c= S & card X = $1 holds

for i2, i3, i4 being Element of F_{1}() holds { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT);

A3: S_{1}[ 0 ]
_{1}[m] holds

S_{1}[m + 1]
_{1}[m]
from NAT_1:sch 2(A3, A6);

then S_{1}[ card S]
;

hence for i2, i3, i4 being Element of F_{1}() holds { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in F_{2}() holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT)
; :: thesis: verum

defpred S

for i2, i3, i4 being Element of F

P

A3: S

proof

A6:
for m being Nat st S
let X be finite set ; :: thesis: ( X c= S & card X = 0 implies for i2, i3, i4 being Element of F_{1}() holds { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT) )

assume A4: ( X c= S & card X = 0 ) ; :: thesis: for i2, i3, i4 being Element of F_{1}() holds { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT)

let i2, i3, i4 be Element of F_{1}(); :: thesis: { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT)

set PP = { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } ;

A5: { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } c= [#] (F_{1}() -xtuples_of NAT)
_{1}() -xtuples_of NAT) c= { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] }
_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT)
by A5, XBOOLE_0:def 10; :: thesis: verum

end;P

assume A4: ( X c= S & card X = 0 ) ; :: thesis: for i2, i3, i4 being Element of F

P

let i2, i3, i4 be Element of F

P

set PP = { p where p is F

P

A5: { p where p is F

P

proof

[#] (F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } or x in [#] (F_{1}() -xtuples_of NAT) )

assume x in { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] }
; :: thesis: x in [#] (F_{1}() -xtuples_of NAT)

then ex p being F_{1}() -element XFinSequence of NAT st

( x = p & ( for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] ) )
;

hence x in [#] (F_{1}() -xtuples_of NAT)
by HILB10_2:def 5; :: thesis: verum

end;P

assume x in { p where p is F

P

then ex p being F

( x = p & ( for i being Nat st i in X holds

P

hence x in [#] (F

P

proof

hence
{ p where p is F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (F_{1}() -xtuples_of NAT) or x in { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } )

assume x in [#] (F_{1}() -xtuples_of NAT)
; :: thesis: x in { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] }

then reconsider p = x as F_{1}() -element XFinSequence of NAT ;

X = {} by A4;

then for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4]
by XBOOLE_0:def 1;

hence x in { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] }
; :: thesis: verum

end;P

assume x in [#] (F

P

then reconsider p = x as F

X = {} by A4;

then for i being Nat st i in X holds

P

hence x in { p where p is F

P

P

S

proof

for m being Nat holds S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A7: S_{1}[m]
; :: thesis: S_{1}[m + 1]

let X be finite set ; :: thesis: ( X c= S & card X = m + 1 implies for i2, i3, i4 being Element of F_{1}() holds { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT) )

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

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT)

let i2, i3, i4 be Element of F_{1}(); :: thesis: { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -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 F_{1}() by A2;

defpred S_{2}[ XFinSequence of NAT ] means for i being Nat st i in X \ {x} holds

P_{1}[$1 . i,$1 . i2,$1 . i3,$1 . i4];

card (X \ {x}) = m by A8, A9, STIRL2_1:55;

then A10: { p where p is F_{1}() -element XFinSequence of NAT : S_{2}[p] } is diophantine Subset of (F_{1}() -xtuples_of NAT)
by A8, XBOOLE_1:1, A7;

defpred S_{3}[ XFinSequence of NAT ] means P_{1}[$1 . x,$1 . i2,$1 . i3,$1 . i4];

A11: { p where p is F_{1}() -element XFinSequence of NAT : S_{3}[p] } is diophantine Subset of (F_{1}() -xtuples_of NAT)
by A1;

defpred S_{4}[ XFinSequence of NAT ] means ( S_{2}[$1] & S_{3}[$1] );

A12: { p where p is F_{1}() -element XFinSequence of NAT : ( S_{2}[p] & S_{3}[p] ) } is diophantine Subset of (F_{1}() -xtuples_of NAT)
from HILB10_3:sch 3(A10, A11);

defpred S_{5}[ XFinSequence of NAT ] means for i being Nat st i in X holds

P_{1}[$1 . i,$1 . i2,$1 . i3,$1 . i4];

A13: for p being F_{1}() -element XFinSequence of NAT holds

( S_{4}[p] iff S_{5}[p] )
_{1}() -element XFinSequence of NAT : S_{4}[p] } = { p where p is F_{1}() -element XFinSequence of NAT : S_{5}[p] }
from HILB10_3:sch 2(A13);

hence { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in X holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT)
by A12; :: thesis: verum

end;assume A7: S

let X be finite set ; :: thesis: ( X c= S & card X = m + 1 implies for i2, i3, i4 being Element of F

P

assume A8: ( X c= S & card X = m + 1 ) ; :: thesis: for i2, i3, i4 being Element of F

P

let i2, i3, i4 be Element of F

P

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 F

defpred S

P

card (X \ {x}) = m by A8, A9, STIRL2_1:55;

then A10: { p where p is F

defpred S

A11: { p where p is F

defpred S

A12: { p where p is F

defpred S

P

A13: for p being F

( S

proof

{ p where p is F
let p be F_{1}() -element XFinSequence of NAT ; :: thesis: ( S_{4}[p] iff S_{5}[p] )

thus ( S_{4}[p] implies S_{5}[p] )
:: thesis: ( S_{5}[p] implies S_{4}[p] )_{5}[p]
; :: thesis: S_{4}[p]

hence S_{4}[p]
by A9, A2; :: thesis: verum

end;thus ( S

proof

assume
S
assume A14:
S_{4}[p]
; :: thesis: S_{5}[p]

let i be Nat; :: thesis: ( i in X implies P_{1}[p . i,p . i2,p . i3,p . i4] )

assume A15: i in X ; :: thesis: P_{1}[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 P_{1}[p . i,p . i2,p . i3,p . i4]
by A14; :: thesis: verum

end;let i be Nat; :: thesis: ( i in X implies P

assume A15: i in X ; :: thesis: P

( 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 P

hence S

hence { p where p is F

P

then S

hence for i2, i3, i4 being Element of F

P