set N = 17;
set EB = EmptyBag 17;
set VARs = 17 \ 8;
A1: for n being Nat holds
( n in 17 \ 8 iff ( 8 <= n & n < 17 ) )

proof

let n be Nat; :: thesis: ( n in 17 \ 8 iff ( 8 <= n & n < 17 ) )
thus ( n in 17 \ 8 implies ( 8 <= n & n < 17 ) ) :: thesis: ( 8 <= n & n < 17 implies n in 17 \ 8 )

proof

assume n in 17 \ 8 ; :: thesis: ( 8 <= n & n < 17 )
then ( n in Segm 17 & not n in Segm 8 ) by XBOOLE_0:def 5;
hence ( 8 <= n & n < 17 ) by NAT_1:44; :: thesis: verum

end;

assume ( 8 <= n & n < 17 ) ; :: thesis: n in 17 \ 8
then ( n in Segm 17 & not n in Segm 8 ) by NAT_1:44;
hence n in 17 \ 8 by XBOOLE_0:def 5; :: thesis: verum

end;

set k = 8;
set Pk = Monom ((1. F_Real),((EmptyBag 17) +* (8,1)));
A2: vars (Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) c= 17 \ 8

proof

( vars (Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) c= {8} & {8} c= 17 \ 8 ) by A1, Th48, ZFMISC_1:31;
hence vars (Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) c= 17 \ 8 ; :: thesis: verum

end;

A3: for x being Function of 17,F_Real holds eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x) = x /. 8

proof

let x be Function of 17,F_Real; :: thesis: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x) = x /. 8
8 in 17 \ 8 by A1;
then eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x) = (1. F_Real) * (x /. 8) by Th27;
hence eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x) = x /. 8 ; :: thesis: verum

end;

set f = 9;
set Pf = Monom ((1. F_Real),((EmptyBag 17) +* (9,1)));
A4: vars (Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) c= 17 \ 8

proof

( vars (Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) c= {9} & {9} c= 17 \ 8 ) by A1, Th48, ZFMISC_1:31;
hence vars (Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) c= 17 \ 8 ; :: thesis: verum

end;

A5: for x being Function of 17,F_Real holds eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x) = x /. 9

proof

let x be Function of 17,F_Real; :: thesis: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x) = x /. 9
9 in 17 \ 8 by A1;
then eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x) = (1. F_Real) * (x /. 9) by Th27;
hence eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x) = x /. 9 ; :: thesis: verum

end;

set i = 10;
set Pi = Monom ((1. F_Real),((EmptyBag 17) +* (10,1)));
A6: vars (Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) c= 17 \ 8

proof

( vars (Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) c= {10} & {10} c= 17 \ 8 ) by A1, Th48, ZFMISC_1:31;
hence vars (Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) c= 17 \ 8 ; :: thesis: verum

end;

A7: for x being Function of 17,F_Real holds eval ((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))),x) = x /. 10

proof

let x be Function of 17,F_Real; :: thesis: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))),x) = x /. 10
10 in 17 \ 8 by A1;
then eval ((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))),x) = (1. F_Real) * (x /. 10) by Th27;
hence eval ((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))),x) = x /. 10 ; :: thesis: verum

end;

set j = 11;
set Pj = Monom ((1. F_Real),((EmptyBag 17) +* (11,1)));
A8: vars (Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) c= 17 \ 8

proof

( vars (Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) c= {11} & {11} c= 17 \ 8 ) by A1, Th48, ZFMISC_1:31;
hence vars (Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) c= 17 \ 8 ; :: thesis: verum

end;

A9: for x being Function of 17,F_Real holds eval ((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))),x) = x /. 11

proof

let x be Function of 17,F_Real; :: thesis: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))),x) = x /. 11
11 in 17 \ 8 by A1;
then eval ((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))),x) = (1. F_Real) * (x /. 11) by Th27;
hence eval ((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))),x) = x /. 11 ; :: thesis: verum

end;

set m = 12;
set Pm = Monom ((1. F_Real),((EmptyBag 17) +* (12,1)));
A10: vars (Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) c= 17 \ 8

proof

( vars (Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) c= {12} & {12} c= 17 \ 8 ) by A1, Th48, ZFMISC_1:31;
hence vars (Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) c= 17 \ 8 ; :: thesis: verum

end;

A11: for x being Function of 17,F_Real holds eval ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))),x) = x /. 12

proof

let x be Function of 17,F_Real; :: thesis: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))),x) = x /. 12
12 in 17 \ 8 by A1;
then eval ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))),x) = (1. F_Real) * (x /. 12) by Th27;
hence eval ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))),x) = x /. 12 ; :: thesis: verum

end;

set u = 13;
set Pu = Monom ((1. F_Real),((EmptyBag 17) +* (13,1)));
A12: vars (Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) c= 17 \ 8

proof

( vars (Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) c= {13} & {13} c= 17 \ 8 ) by A1, Th48, ZFMISC_1:31;
hence vars (Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) c= 17 \ 8 ; :: thesis: verum

end;

A13: for x being Function of 17,F_Real holds eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x) = x /. 13

proof

let x be Function of 17,F_Real; :: thesis: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x) = x /. 13
13 in 17 \ 8 by A1;
then eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x) = (1. F_Real) * (x /. 13) by Th27;
hence eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x) = x /. 13 ; :: thesis: verum

end;

set r = 14;
set Pr = Monom ((1. F_Real),((EmptyBag 17) +* (14,1)));
A14: vars (Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) c= 17 \ 8

proof

( vars (Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) c= {14} & {14} c= 17 \ 8 ) by A1, Th48, ZFMISC_1:31;
hence vars (Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) c= 17 \ 8 ; :: thesis: verum

end;

A15: for x being Function of 17,F_Real holds eval ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))),x) = x /. 14

proof

let x be Function of 17,F_Real; :: thesis: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))),x) = x /. 14
14 in 17 \ 8 by A1;
then eval ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))),x) = (1. F_Real) * (x /. 14) by Th27;
hence eval ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))),x) = x /. 14 ; :: thesis: verum

end;

set s = 15;
set Ps = Monom ((1. F_Real),((EmptyBag 17) +* (15,1)));
A16: vars (Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))) c= 17 \ 8

proof

( vars (Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))) c= {15} & {15} c= 17 \ 8 ) by A1, Th48, ZFMISC_1:31;
hence vars (Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))) c= 17 \ 8 ; :: thesis: verum

end;

A17: for x being Function of 17,F_Real holds eval ((Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))),x) = x /. 15

proof

let x be Function of 17,F_Real; :: thesis: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))),x) = x /. 15
15 in 17 \ 8 by A1;
then eval ((Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))),x) = (1. F_Real) * (x /. 15) by Th27;
hence eval ((Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))),x) = x /. 15 ; :: thesis: verum

end;

set t = 16;
set Pt = Monom ((1. F_Real),((EmptyBag 17) +* (16,1)));
A18: vars (Monom ((1. F_Real),((EmptyBag 17) +* (16,1)))) c= 17 \ 8

proof

( vars (Monom ((1. F_Real),((EmptyBag 17) +* (16,1)))) c= {16} & {16} c= 17 \ 8 ) by A1, Th48, ZFMISC_1:31;
hence vars (Monom ((1. F_Real),((EmptyBag 17) +* (16,1)))) c= 17 \ 8 ; :: thesis: verum

end;

A19: for x being Function of 17,F_Real holds eval ((Monom ((1. F_Real),((EmptyBag 17) +* (16,1)))),x) = x /. 16

proof

let x be Function of 17,F_Real; :: thesis: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (16,1)))),x) = x /. 16
16 in 17 \ 8 by A1;
then eval ((Monom ((1. F_Real),((EmptyBag 17) +* (16,1)))),x) = (1. F_Real) * (x /. 16) by Th27;
hence eval ((Monom ((1. F_Real),((EmptyBag 17) +* (16,1)))),x) = x /. 16 ; :: thesis: verum

end;

reconsider Hund = 100 as integer Element of F_Real by XREAL_0:def 1;
set O = 1_ (17,F_Real);
A20: vars (1_ (17,F_Real)) c= 17 \ 8 by Th38;
reconsider W = Hund * (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))) as INT -valued Polynomial of 17,F_Real ;
A21: vars W c= 17 \ 8

proof

( vars ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))) c= 17 \ 8 & vars ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real))) c= 17 \ 8 ) by A20, A4, A2, Th79, Th78;
then vars (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))) c= 17 \ 8 by Th79;
hence vars W c= 17 \ 8 by Th80; :: thesis: verum

end;

A22: for x being Function of 17,F_Real holds eval (W,x) = ((Hund * (x /. 9)) * (x /. 8)) * ((x /. 8) + (1. F_Real))

proof

let x be Function of 17,F_Real; :: thesis: eval (W,x) = ((Hund * (x /. 9)) * (x /. 8)) * ((x /. 8) + (1. F_Real))
thus eval (W,x) = Hund * (eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))),x)) by POLYNOM7:29
.= Hund * ((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))),x)) * (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real))),x))) by POLYNOM2:25
.= Hund * ((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))),x)) * ((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x)) + (eval ((1_ (17,F_Real)),x)))) by POLYNOM2:23
.= Hund * ((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))),x)) * ((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x)) + (1. F_Real))) by POLYNOM2:21
.= Hund * ((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))),x)) * ((x /. 8) + (1. F_Real))) by A3
.= Hund * (((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x)) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x))) * ((x /. 8) + (1. F_Real))) by POLYNOM2:25
.= Hund * (((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x)) * (x /. 8)) * ((x /. 8) + (1. F_Real))) by A3
.= Hund * (((x /. 9) * (x /. 8)) * ((x /. 8) + (1. F_Real))) by A5
.= ((Hund * (x /. 9)) * (x /. 8)) * ((x /. 8) + (1. F_Real)) ; :: thesis: verum

end;

reconsider U = (Hund * ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' ((W *' W) *' W))) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A23: vars U c= 17 \ 8

proof

( vars ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) c= 17 \ 8 & vars (W *' W) c= 17 \ 8 ) by A21, A12, Th79;
then ( vars (((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) c= 17 \ 8 & vars ((W *' W) *' W) c= 17 \ 8 ) by A21, A12, Th79;
then vars ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' ((W *' W) *' W)) c= 17 \ 8 by Th79;
then vars (Hund * ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' ((W *' W) *' W))) c= 17 \ 8 by Th80;
hence vars U c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A24: for x being Function of 17,F_Real holds eval (U,x) = ((Hund * ((x /. 13) |^ 3)) * ((eval (W,x)) |^ 3)) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (U,x) = ((Hund * ((x /. 13) |^ 3)) * ((eval (W,x)) |^ 3)) + (1. F_Real)
A25: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x) = x /. 13 by A13;
A26: eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))),x) = (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))),x)) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x)) by POLYNOM2:25
.= ((x /. 13) * (x /. 13)) * (x /. 13) by A25, POLYNOM2:25
.= ((x /. 13) |^ (1 + 1)) * ((x /. 13) |^ 1) by NEWTON:6
.= (x /. 13) |^ ((1 + 1) + 1) by NEWTON:6 ;
A27: eval (((W *' W) *' W),x) = (eval ((W *' W),x)) * (eval (W,x)) by POLYNOM2:25
.= ((eval (W,x)) * (eval (W,x))) * (eval (W,x)) by POLYNOM2:25
.= ((eval (W,x)) |^ (1 + 1)) * ((eval (W,x)) |^ 1) by NEWTON:6
.= (eval (W,x)) |^ ((1 + 1) + 1) by NEWTON:6 ;
thus eval (U,x) = (eval ((Hund * ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' ((W *' W) *' W))),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval ((Hund * ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' ((W *' W) *' W))),x)) + (1. F_Real) by POLYNOM2:21
.= (Hund * (eval (((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' ((W *' W) *' W)),x))) + (1. F_Real) by POLYNOM7:29
.= (Hund * ((eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))),x)) * (eval (((W *' W) *' W),x)))) + (1. F_Real) by POLYNOM2:25
.= ((Hund * ((x /. 13) |^ 3)) * ((eval (W,x)) |^ 3)) + (1. F_Real) by A26, A27 ; :: thesis: verum

end;

reconsider M = (Hund * (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' U) *' W)) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A28: vars M c= 17 \ 8

proof

vars ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' U) c= 17 \ 8 by A23, A10, Th79;
then vars (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' U) *' W) c= 17 \ 8 by A21, Th79;
then vars (Hund * (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' U) *' W)) c= 17 \ 8 by Th80;
hence vars M c= 17 \ 8 by Th78, A20; :: thesis: verum

end;

A29: for x being Function of 17,F_Real holds eval (M,x) = (((Hund * (x /. 12)) * (eval (U,x))) * (eval (W,x))) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (M,x) = (((Hund * (x /. 12)) * (eval (U,x))) * (eval (W,x))) + (1. F_Real)
thus eval (M,x) = (eval ((Hund * (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' U) *' W)),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval ((Hund * (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' U) *' W)),x)) + (1. F_Real) by POLYNOM2:21
.= (Hund * (eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' U) *' W),x))) + (1. F_Real) by POLYNOM7:29
.= (Hund * ((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' U),x)) * (eval (W,x)))) + (1. F_Real) by POLYNOM2:25
.= (Hund * (((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))),x)) * (eval (U,x))) * (eval (W,x)))) + (1. F_Real) by POLYNOM2:25
.= (Hund * (((x /. 12) * (eval (U,x))) * (eval (W,x)))) + (1. F_Real) by A11
.= (((Hund * (x /. 12)) * (eval (U,x))) * (eval (W,x))) + (1. F_Real) ; :: thesis: verum

end;

reconsider S = (((M - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (15,1))))) + (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A30: vars S c= 17 \ 8

proof

vars (M - (1_ (17,F_Real))) c= 17 \ 8 by Th81, A28, A20;
then vars ((M - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (15,1))))) c= 17 \ 8 by A16, Th79;
then vars (((M - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (15,1))))) + (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))) c= 17 \ 8 by A2, Th78;
hence vars S c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A31: for x being Function of 17,F_Real holds eval (S,x) = ((((eval (M,x)) - (1. F_Real)) * (x /. 15)) + (x /. 8)) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (S,x) = ((((eval (M,x)) - (1. F_Real)) * (x /. 15)) + (x /. 8)) + (1. F_Real)
thus eval (S,x) = (eval ((((M - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (15,1))))) + (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval ((((M - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (15,1))))) + (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))),x)) + (1. F_Real) by POLYNOM2:21
.= ((eval (((M - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (15,1))))),x)) + (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x))) + (1. F_Real) by POLYNOM2:23
.= ((eval (((M - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (15,1))))),x)) + (x /. 8)) + (1. F_Real) by A3
.= (((eval ((M - (1_ (17,F_Real))),x)) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))),x))) + (x /. 8)) + (1. F_Real) by POLYNOM2:25
.= ((((eval (M,x)) - (eval ((1_ (17,F_Real)),x))) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))),x))) + (x /. 8)) + (1. F_Real) by POLYNOM2:24
.= ((((eval (M,x)) - (1. F_Real)) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (15,1)))),x))) + (x /. 8)) + (1. F_Real) by POLYNOM2:21
.= ((((eval (M,x)) - (1. F_Real)) * (x /. 15)) + (x /. 8)) + (1. F_Real) by A17 ; :: thesis: verum

end;

reconsider T = (((((M *' U) - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (16,1))))) + W) - (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A32: vars T c= 17 \ 8

proof

vars (M *' U) c= 17 \ 8 by A23, A28, Th79;
then vars ((M *' U) - (1_ (17,F_Real))) c= 17 \ 8 by A20, Th81;
then vars (((M *' U) - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (16,1))))) c= 17 \ 8 by A18, Th79;
then vars ((((M *' U) - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (16,1))))) + W) c= 17 \ 8 by A21, Th78;
then vars (((((M *' U) - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (16,1))))) + W) - (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))) c= 17 \ 8 by Th81, A2;
hence vars T c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A33: for x being Function of 17,F_Real holds eval (T,x) = ((((((eval (M,x)) * (eval (U,x))) - (1. F_Real)) * (x /. 16)) + (eval (W,x))) - (x /. 8)) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (T,x) = ((((((eval (M,x)) * (eval (U,x))) - (1. F_Real)) * (x /. 16)) + (eval (W,x))) - (x /. 8)) + (1. F_Real)
thus eval (T,x) = (eval ((((((M *' U) - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (16,1))))) + W) - (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval ((((((M *' U) - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (16,1))))) + W) - (Monom ((1. F_Real),((EmptyBag 17) +* (8,1))))),x)) + (1. F_Real) by POLYNOM2:21
.= ((eval (((((M *' U) - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (16,1))))) + W),x)) - (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x))) + (1. F_Real) by POLYNOM2:24
.= ((eval (((((M *' U) - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (16,1))))) + W),x)) - (x /. 8)) + (1. F_Real) by A3
.= (((eval ((((M *' U) - (1_ (17,F_Real))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (16,1))))),x)) + (eval (W,x))) - (x /. 8)) + (1. F_Real) by POLYNOM2:23
.= ((((eval (((M *' U) - (1_ (17,F_Real))),x)) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (16,1)))),x))) + (eval (W,x))) - (x /. 8)) + (1. F_Real) by POLYNOM2:25
.= ((((eval (((M *' U) - (1_ (17,F_Real))),x)) * (x /. 16)) + (eval (W,x))) - (x /. 8)) + (1. F_Real) by A19
.= (((((eval ((M *' U),x)) - (eval ((1_ (17,F_Real)),x))) * (x /. 16)) + (eval (W,x))) - (x /. 8)) + (1. F_Real) by POLYNOM2:24
.= (((((eval ((M *' U),x)) - (1. F_Real)) * (x /. 16)) + (eval (W,x))) - (x /. 8)) + (1. F_Real) by POLYNOM2:21
.= ((((((eval (M,x)) * (eval (U,x))) - (1. F_Real)) * (x /. 16)) + (eval (W,x))) - (x /. 8)) + (1. F_Real) by POLYNOM2:25 ; :: thesis: verum

end;

reconsider Two = 2 as integer Element of F_Real by XREAL_0:def 1;
reconsider Q = ((Two * (M *' W)) - (W *' W)) - (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A34: vars Q c= 17 \ 8

proof

vars (M *' W) c= 17 \ 8 by A28, A21, Th79;
then ( vars (Two * (M *' W)) c= 17 \ 8 & vars (W *' W) c= 17 \ 8 ) by A21, Th79, Th80;
then vars ((Two * (M *' W)) - (W *' W)) c= 17 \ 8 by Th81;
hence vars Q c= 17 \ 8 by A20, Th81; :: thesis: verum

end;

A35: for x being Function of 17,F_Real holds eval (Q,x) = (((Two * (eval (M,x))) * (eval (W,x))) - ((eval (W,x)) ^2)) - (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (Q,x) = (((Two * (eval (M,x))) * (eval (W,x))) - ((eval (W,x)) ^2)) - (1. F_Real)
thus eval (Q,x) = (eval (((Two * (M *' W)) - (W *' W)),x)) - (eval ((1_ (17,F_Real)),x)) by POLYNOM2:24
.= (eval (((Two * (M *' W)) - (W *' W)),x)) - (1. F_Real) by POLYNOM2:21
.= ((eval ((Two * (M *' W)),x)) - (eval ((W *' W),x))) - (1. F_Real) by POLYNOM2:24
.= ((Two * (eval ((M *' W),x))) - (eval ((W *' W),x))) - (1. F_Real) by POLYNOM7:29
.= ((Two * (eval ((M *' W),x))) - ((eval (W,x)) * (eval (W,x)))) - (1. F_Real) by POLYNOM2:25
.= ((Two * ((eval (M,x)) * (eval (W,x)))) - ((eval (W,x)) * (eval (W,x)))) - (1. F_Real) by POLYNOM2:25
.= (((Two * (eval (M,x))) * (eval (W,x))) - ((eval (W,x)) ^2)) - (1. F_Real) by SQUARE_1:def 1 ; :: thesis: verum

end;

reconsider L = ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real))) *' Q as INT -valued Polynomial of 17,F_Real ;
A36: vars L c= 17 \ 8

proof

vars ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real))) c= 17 \ 8 by A2, A20, Th78;
hence vars L c= 17 \ 8 by A34, Th79; :: thesis: verum

end;

A37: for x being Function of 17,F_Real holds eval (L,x) = ((x /. 8) + (1. F_Real)) * (eval (Q,x))

proof

let x be Function of 17,F_Real; :: thesis: eval (L,x) = ((x /. 8) + (1. F_Real)) * (eval (Q,x))
thus eval (L,x) = (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real))),x)) * (eval (Q,x)) by POLYNOM2:25
.= ((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x)) + (eval ((1_ (17,F_Real)),x))) * (eval (Q,x)) by POLYNOM2:23
.= ((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x)) + (1. F_Real)) * (eval (Q,x)) by POLYNOM2:21
.= ((x /. 8) + (1. F_Real)) * (eval (Q,x)) by A3 ; :: thesis: verum

end;

reconsider A = M *' (U + (1_ (17,F_Real))) as INT -valued Polynomial of 17,F_Real ;
A38: vars A c= 17 \ 8

proof

vars (U + (1_ (17,F_Real))) c= 17 \ 8 by A20, A23, Th78;
hence vars A c= 17 \ 8 by A28, Th79; :: thesis: verum

end;

A39: for x being Function of 17,F_Real holds eval (A,x) = (eval (M,x)) * ((eval (U,x)) + (1. F_Real))

proof

let x be Function of 17,F_Real; :: thesis: eval (A,x) = (eval (M,x)) * ((eval (U,x)) + (1. F_Real))
thus eval (A,x) = (eval (M,x)) * (eval ((U + (1_ (17,F_Real))),x)) by POLYNOM2:25
.= (eval (M,x)) * ((eval (U,x)) + (eval ((1_ (17,F_Real)),x))) by POLYNOM2:23
.= (eval (M,x)) * ((eval (U,x)) + (1. F_Real)) by POLYNOM2:21 ; :: thesis: verum

end;

reconsider B = W + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A40: vars B c= 17 \ 8 by A20, A21, Th78;
A41: for x being Function of 17,F_Real holds eval (B,x) = (eval (W,x)) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (B,x) = (eval (W,x)) + (1. F_Real)
thus eval (B,x) = (eval (W,x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval (W,x)) + (1. F_Real) by POLYNOM2:21 ; :: thesis: verum

end;

reconsider C = ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) + W) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A42: vars C c= 17 \ 8

proof

vars ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) + W) c= 17 \ 8 by A14, A21, Th78;
hence vars C c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A43: for x being Function of 17,F_Real holds eval (C,x) = ((x /. 14) + (eval (W,x))) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (C,x) = ((x /. 14) + (eval (W,x))) + (1. F_Real)
thus eval (C,x) = (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) + W),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) + W),x)) + (1. F_Real) by POLYNOM2:21
.= ((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))),x)) + (eval (W,x))) + (1. F_Real) by POLYNOM2:23
.= ((x /. 14) + (eval (W,x))) + (1. F_Real) by A15 ; :: thesis: verum

end;

reconsider D = (((A *' A) - (1_ (17,F_Real))) *' (C *' C)) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A44: vars D c= 17 \ 8

proof

vars (A *' A) c= 17 \ 8 by A38, Th79;
then ( vars ((A *' A) - (1_ (17,F_Real))) c= 17 \ 8 & vars (C *' C) c= 17 \ 8 ) by A42, A20, Th81, Th79;
then vars (((A *' A) - (1_ (17,F_Real))) *' (C *' C)) c= 17 \ 8 by Th79;
hence vars D c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A45: for x being Function of 17,F_Real holds eval (D,x) = ((((eval (A,x)) ^2) - (1. F_Real)) * ((eval (C,x)) ^2)) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (D,x) = ((((eval (A,x)) ^2) - (1. F_Real)) * ((eval (C,x)) ^2)) + (1. F_Real)
thus eval (D,x) = (eval ((((A *' A) - (1_ (17,F_Real))) *' (C *' C)),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval ((((A *' A) - (1_ (17,F_Real))) *' (C *' C)),x)) + (1. F_Real) by POLYNOM2:21
.= ((eval (((A *' A) - (1_ (17,F_Real))),x)) * (eval ((C *' C),x))) + (1. F_Real) by POLYNOM2:25
.= ((eval (((A *' A) - (1_ (17,F_Real))),x)) * ((eval (C,x)) * (eval (C,x)))) + (1. F_Real) by POLYNOM2:25
.= (((eval ((A *' A),x)) - (eval ((1_ (17,F_Real)),x))) * ((eval (C,x)) * (eval (C,x)))) + (1. F_Real) by POLYNOM2:24
.= (((eval ((A *' A),x)) - (eval ((1_ (17,F_Real)),x))) * ((eval (C,x)) ^2)) + (1. F_Real) by SQUARE_1:def 1
.= (((eval ((A *' A),x)) - (1. F_Real)) * ((eval (C,x)) ^2)) + (1. F_Real) by POLYNOM2:21
.= ((((eval (A,x)) * (eval (A,x))) - (1. F_Real)) * ((eval (C,x)) ^2)) + (1. F_Real) by POLYNOM2:25
.= ((((eval (A,x)) ^2) - (1. F_Real)) * ((eval (C,x)) ^2)) + (1. F_Real) by SQUARE_1:def 1 ; :: thesis: verum

end;

reconsider E = Two * (((((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) *' C) *' C) *' L) *' D) as INT -valued Polynomial of 17,F_Real ;
A46: vars E c= 17 \ 8

proof

vars ((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) *' C) c= 17 \ 8 by A42, A6, Th79;
then vars (((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) *' C) *' C) c= 17 \ 8 by A42, Th79;
then vars ((((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) *' C) *' C) *' L) c= 17 \ 8 by A36, Th79;
then vars (((((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) *' C) *' C) *' L) *' D) c= 17 \ 8 by A44, Th79;
hence vars E c= 17 \ 8 by Th80; :: thesis: verum

end;

A47: for x being Function of 17,F_Real holds eval (E,x) = (((Two * (x /. 10)) * ((eval (C,x)) ^2)) * (eval (L,x))) * (eval (D,x))

proof

let x be Function of 17,F_Real; :: thesis: eval (E,x) = (((Two * (x /. 10)) * ((eval (C,x)) ^2)) * (eval (L,x))) * (eval (D,x))
A48: (eval (C,x)) * (eval (C,x)) = (eval (C,x)) ^2 by SQUARE_1:def 1;
thus eval (E,x) = Two * (eval ((((((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) *' C) *' C) *' L) *' D),x)) by POLYNOM7:29
.= Two * ((eval (((((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) *' C) *' C) *' L),x)) * (eval (D,x))) by POLYNOM2:25
.= Two * (((eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) *' C) *' C),x)) * (eval (L,x))) * (eval (D,x))) by POLYNOM2:25
.= Two * ((((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))) *' C),x)) * (eval (C,x))) * (eval (L,x))) * (eval (D,x))) by POLYNOM2:25
.= Two * (((((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))),x)) * (eval (C,x))) * (eval (C,x))) * (eval (L,x))) * (eval (D,x))) by POLYNOM2:25
.= Two * ((((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (10,1)))),x)) * ((eval (C,x)) * (eval (C,x)))) * (eval (L,x))) * (eval (D,x)))
.= Two * ((((x /. 10) * ((eval (C,x)) * (eval (C,x)))) * (eval (L,x))) * (eval (D,x))) by A7
.= (((Two * (x /. 10)) * ((eval (C,x)) ^2)) * (eval (L,x))) * (eval (D,x)) by A48 ; :: thesis: verum

end;

reconsider F = (((A *' A) - (1_ (17,F_Real))) *' (E *' E)) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A49: vars F c= 17 \ 8

proof

vars (A *' A) c= 17 \ 8 by A38, Th79;
then ( vars ((A *' A) - (1_ (17,F_Real))) c= 17 \ 8 & vars (E *' E) c= 17 \ 8 ) by A46, A20, Th81, Th79;
then vars (((A *' A) - (1_ (17,F_Real))) *' (E *' E)) c= 17 \ 8 by Th79;
hence vars F c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A50: for x being Function of 17,F_Real holds eval (F,x) = ((((eval (A,x)) ^2) - (1. F_Real)) * ((eval (E,x)) ^2)) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (F,x) = ((((eval (A,x)) ^2) - (1. F_Real)) * ((eval (E,x)) ^2)) + (1. F_Real)
thus eval (F,x) = (eval ((((A *' A) - (1_ (17,F_Real))) *' (E *' E)),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval ((((A *' A) - (1_ (17,F_Real))) *' (E *' E)),x)) + (1. F_Real) by POLYNOM2:21
.= ((eval (((A *' A) - (1_ (17,F_Real))),x)) * (eval ((E *' E),x))) + (1. F_Real) by POLYNOM2:25
.= ((eval (((A *' A) - (1_ (17,F_Real))),x)) * ((eval (E,x)) * (eval (E,x)))) + (1. F_Real) by POLYNOM2:25
.= ((eval (((A *' A) - (1_ (17,F_Real))),x)) * ((eval (E,x)) ^2)) + (1. F_Real) by SQUARE_1:def 1
.= (((eval ((A *' A),x)) - (eval ((1_ (17,F_Real)),x))) * ((eval (E,x)) ^2)) + (1. F_Real) by POLYNOM2:24
.= (((eval ((A *' A),x)) - (1. F_Real)) * ((eval (E,x)) ^2)) + (1. F_Real) by POLYNOM2:21
.= ((((eval (A,x)) * (eval (A,x))) - (1. F_Real)) * ((eval (E,x)) ^2)) + (1. F_Real) by POLYNOM2:25
.= ((((eval (A,x)) ^2) - (1. F_Real)) * ((eval (E,x)) ^2)) + (1. F_Real) by SQUARE_1:def 1 ; :: thesis: verum

end;

reconsider G = A + (F *' (F - A)) as INT -valued Polynomial of 17,F_Real ;
A51: vars G c= 17 \ 8

proof

vars (F - A) c= 17 \ 8 by A38, A49, Th81;
then vars (F *' (F - A)) c= 17 \ 8 by A49, Th79;
hence vars G c= 17 \ 8 by A38, Th78; :: thesis: verum

end;

A52: for x being Function of 17,F_Real holds eval (G,x) = (eval (A,x)) + ((eval (F,x)) * ((eval (F,x)) - (eval (A,x))))

proof

let x be Function of 17,F_Real; :: thesis: eval (G,x) = (eval (A,x)) + ((eval (F,x)) * ((eval (F,x)) - (eval (A,x))))
thus eval (G,x) = (eval (A,x)) + (eval ((F *' (F - A)),x)) by POLYNOM2:23
.= (eval (A,x)) + ((eval (F,x)) * (eval ((F - A),x))) by POLYNOM2:25
.= (eval (A,x)) + ((eval (F,x)) * ((eval (F,x)) - (eval (A,x)))) by POLYNOM2:24 ; :: thesis: verum

end;

reconsider H = B + (Two * (((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) - (1_ (17,F_Real))) *' C)) as INT -valued Polynomial of 17,F_Real ;
A53: vars H c= 17 \ 8

proof

vars ((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) - (1_ (17,F_Real))) c= 17 \ 8 by A8, A20, Th81;
then vars (((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) - (1_ (17,F_Real))) *' C) c= 17 \ 8 by A42, Th79;
then vars (Two * (((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) - (1_ (17,F_Real))) *' C)) c= 17 \ 8 by Th80;
hence vars H c= 17 \ 8 by A40, Th78; :: thesis: verum

end;

A54: for x being Function of 17,F_Real holds eval (H,x) = (eval (B,x)) + ((Two * ((x /. 11) - (1. F_Real))) * (eval (C,x)))

proof

let x be Function of 17,F_Real; :: thesis: eval (H,x) = (eval (B,x)) + ((Two * ((x /. 11) - (1. F_Real))) * (eval (C,x)))
thus eval (H,x) = (eval (B,x)) + (eval ((Two * (((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) - (1_ (17,F_Real))) *' C)),x)) by POLYNOM2:23
.= (eval (B,x)) + (Two * (eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) - (1_ (17,F_Real))) *' C),x))) by POLYNOM7:29
.= (eval (B,x)) + (Two * ((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))) - (1_ (17,F_Real))),x)) * (eval (C,x)))) by POLYNOM2:25
.= (eval (B,x)) + (Two * (((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))),x)) - (eval ((1_ (17,F_Real)),x))) * (eval (C,x)))) by POLYNOM2:24
.= (eval (B,x)) + (Two * (((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (11,1)))),x)) - (1. F_Real)) * (eval (C,x)))) by POLYNOM2:21
.= (eval (B,x)) + (Two * (((x /. 11) - (1. F_Real)) * (eval (C,x)))) by A9
.= (eval (B,x)) + ((Two * ((x /. 11) - (1. F_Real))) * (eval (C,x))) ; :: thesis: verum

end;

reconsider I = (((G *' G) - (1_ (17,F_Real))) *' (H *' H)) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A55: vars I c= 17 \ 8

proof

vars (G *' G) c= 17 \ 8 by A51, Th79;
then ( vars ((G *' G) - (1_ (17,F_Real))) c= 17 \ 8 & vars (H *' H) c= 17 \ 8 ) by A53, A20, Th81, Th79;
then vars (((G *' G) - (1_ (17,F_Real))) *' (H *' H)) c= 17 \ 8 by Th79;
hence vars I c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A56: for x being Function of 17,F_Real holds eval (I,x) = ((((eval (G,x)) ^2) - (1. F_Real)) * ((eval (H,x)) ^2)) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (I,x) = ((((eval (G,x)) ^2) - (1. F_Real)) * ((eval (H,x)) ^2)) + (1. F_Real)
thus eval (I,x) = (eval ((((G *' G) - (1_ (17,F_Real))) *' (H *' H)),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval ((((G *' G) - (1_ (17,F_Real))) *' (H *' H)),x)) + (1. F_Real) by POLYNOM2:21
.= ((eval (((G *' G) - (1_ (17,F_Real))),x)) * (eval ((H *' H),x))) + (1. F_Real) by POLYNOM2:25
.= ((eval (((G *' G) - (1_ (17,F_Real))),x)) * ((eval (H,x)) * (eval (H,x)))) + (1. F_Real) by POLYNOM2:25
.= ((eval (((G *' G) - (1_ (17,F_Real))),x)) * ((eval (H,x)) ^2)) + (1. F_Real) by SQUARE_1:def 1
.= (((eval ((G *' G),x)) - (eval ((1_ (17,F_Real)),x))) * ((eval (H,x)) ^2)) + (1. F_Real) by POLYNOM2:24
.= (((eval ((G *' G),x)) - (1. F_Real)) * ((eval (H,x)) ^2)) + (1. F_Real) by POLYNOM2:21
.= ((((eval (G,x)) * (eval (G,x))) - (1. F_Real)) * ((eval (H,x)) ^2)) + (1. F_Real) by POLYNOM2:25
.= ((((eval (G,x)) ^2) - (1. F_Real)) * ((eval (H,x)) ^2)) + (1. F_Real) by SQUARE_1:def 1 ; :: thesis: verum

end;

reconsider X1 = (((M *' M) - (1_ (17,F_Real))) *' (S *' S)) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A57: vars X1 c= 17 \ 8

proof

vars (M *' M) c= 17 \ 8 by A28, Th79;
then ( vars ((M *' M) - (1_ (17,F_Real))) c= 17 \ 8 & vars (S *' S) c= 17 \ 8 ) by A20, Th81, A30, Th79;
then vars (((M *' M) - (1_ (17,F_Real))) *' (S *' S)) c= 17 \ 8 by Th79;
hence vars X1 c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A58: for x being Function of 17,F_Real holds eval (X1,x) = ((((eval (M,x)) ^2) - (1. F_Real)) * ((eval (S,x)) ^2)) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (X1,x) = ((((eval (M,x)) ^2) - (1. F_Real)) * ((eval (S,x)) ^2)) + (1. F_Real)
thus eval (X1,x) = (eval ((((M *' M) - (1_ (17,F_Real))) *' (S *' S)),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval ((((M *' M) - (1_ (17,F_Real))) *' (S *' S)),x)) + (1. F_Real) by POLYNOM2:21
.= ((eval (((M *' M) - (1_ (17,F_Real))),x)) * (eval ((S *' S),x))) + (1. F_Real) by POLYNOM2:25
.= ((eval (((M *' M) - (1_ (17,F_Real))),x)) * ((eval (S,x)) * (eval (S,x)))) + (1. F_Real) by POLYNOM2:25
.= ((eval (((M *' M) - (1_ (17,F_Real))),x)) * ((eval (S,x)) ^2)) + (1. F_Real) by SQUARE_1:def 1
.= (((eval ((M *' M),x)) - (eval ((1_ (17,F_Real)),x))) * ((eval (S,x)) ^2)) + (1. F_Real) by POLYNOM2:24
.= (((eval ((M *' M),x)) - (1. F_Real)) * ((eval (S,x)) ^2)) + (1. F_Real) by POLYNOM2:21
.= ((((eval (M,x)) * (eval (M,x))) - (1. F_Real)) * ((eval (S,x)) ^2)) + (1. F_Real) by POLYNOM2:25
.= ((((eval (M,x)) ^2) - (1. F_Real)) * ((eval (S,x)) ^2)) + (1. F_Real) by SQUARE_1:def 1 ; :: thesis: verum

end;

reconsider X2 = ((((M *' U) *' (M *' U)) - (1_ (17,F_Real))) *' (T *' T)) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A59: vars X2 c= 17 \ 8

proof

vars (M *' U) c= 17 \ 8 by A23, A28, Th79;
then vars ((M *' U) *' (M *' U)) c= 17 \ 8 by Th79;
then ( vars (((M *' U) *' (M *' U)) - (1_ (17,F_Real))) c= 17 \ 8 & vars (T *' T) c= 17 \ 8 ) by A20, Th81, A32, Th79;
then vars ((((M *' U) *' (M *' U)) - (1_ (17,F_Real))) *' (T *' T)) c= 17 \ 8 by Th79;
hence vars X2 c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A60: for x being Function of 17,F_Real holds eval (X2,x) = (((((eval (M,x)) * (eval (U,x))) ^2) - (1. F_Real)) * ((eval (T,x)) ^2)) + (1. F_Real)

proof

let x be Function of 17,F_Real; :: thesis: eval (X2,x) = (((((eval (M,x)) * (eval (U,x))) ^2) - (1. F_Real)) * ((eval (T,x)) ^2)) + (1. F_Real)
eval ((M *' U),x) = (eval (M,x)) * (eval (U,x)) by POLYNOM2:25;
then A61: ( eval (((M *' U) *' (M *' U)),x) = ((eval (M,x)) * (eval (U,x))) * ((eval (M,x)) * (eval (U,x))) & eval ((1_ (17,F_Real)),x) = 1. F_Real & eval ((T *' T),x) = (eval (T,x)) * (eval (T,x)) ) by POLYNOM2:21, POLYNOM2:25;
thus eval (X2,x) = (eval (((((M *' U) *' (M *' U)) - (1_ (17,F_Real))) *' (T *' T)),x)) + (1. F_Real) by POLYNOM2:23, A61
.= ((eval ((((M *' U) *' (M *' U)) - (1_ (17,F_Real))),x)) * (eval ((T *' T),x))) + (1. F_Real) by POLYNOM2:25
.= (((eval (((M *' U) *' (M *' U)),x)) - (1. F_Real)) * (eval ((T *' T),x))) + (1. F_Real) by A61, POLYNOM2:24
.= (((((eval (M,x)) * (eval (U,x))) * ((eval (M,x)) * (eval (U,x)))) - (1. F_Real)) * ((eval (T,x)) ^2)) + (1. F_Real) by A61, SQUARE_1:def 1
.= (((((eval (M,x)) * (eval (U,x))) ^2) - (1. F_Real)) * ((eval (T,x)) ^2)) + (1. F_Real) by SQUARE_1:def 1 ; :: thesis: verum

end;

reconsider X3 = (D *' F) *' I as INT -valued Polynomial of 17,F_Real ;
A62: vars X3 c= 17 \ 8

proof

vars (D *' F) c= 17 \ 8 by A44, A49, Th79;
hence vars X3 c= 17 \ 8 by A55, Th79; :: thesis: verum

end;

A63: for x being Function of 17,F_Real holds eval (X3,x) = ((eval (D,x)) * (eval (F,x))) * (eval (I,x))

proof

let x be Function of 17,F_Real; :: thesis: eval (X3,x) = ((eval (D,x)) * (eval (F,x))) * (eval (I,x))
eval ((D *' F),x) = (eval (D,x)) * (eval (F,x)) by POLYNOM2:25;
hence eval (X3,x) = ((eval (D,x)) * (eval (F,x))) * (eval (I,x)) by POLYNOM2:25; :: thesis: verum

end;

reconsider P = F *' L as INT -valued Polynomial of 17,F_Real ;
A64: vars P c= 17 \ 8 by A49, A36, Th79;
A65: for x being Function of 17,F_Real holds eval (P,x) = (eval (F,x)) * (eval (L,x)) by POLYNOM2:25;
reconsider R = (((H - C) *' L) + ((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) + (1_ (17,F_Real)))) *' Q)) + ((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))) *' ((((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))) + (1_ (17,F_Real)))) as INT -valued Polynomial of 17,F_Real ;
A66: vars R c= 17 \ 8

proof

vars (H - C) c= 17 \ 8 by A53, A42, Th81;
then A67: vars ((H - C) *' L) c= 17 \ 8 by A36, Th79;
vars ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) + (1_ (17,F_Real))) c= 17 \ 8 by A4, A20, Th78;
then vars (F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) + (1_ (17,F_Real)))) c= 17 \ 8 by A49, Th79;
then vars ((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) + (1_ (17,F_Real)))) *' Q) c= 17 \ 8 by A34, Th79;
then A68: vars (((H - C) *' L) + ((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) + (1_ (17,F_Real)))) *' Q)) c= 17 \ 8 by A67, Th78;
vars ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real))) c= 17 \ 8 by A20, A2, Th78;
then A69: vars (F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))) c= 17 \ 8 by A49, Th79;
A70: vars (W *' W) c= 17 \ 8 by A21, Th79;
then vars ((W *' W) - (1_ (17,F_Real))) c= 17 \ 8 by A20, Th81;
then vars (((W *' W) - (1_ (17,F_Real))) *' S) c= 17 \ 8 by A30, Th79;
then A71: vars ((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) c= 17 \ 8 by A12, Th79;
vars ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) c= 17 \ 8 by A12, Th79;
then vars ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))))) c= 17 \ 8 by A70, Th79;
then vars (((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))) c= 17 \ 8 by A71, Th81;
then vars ((((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))) + (1_ (17,F_Real))) c= 17 \ 8 by A20, Th78;
then vars ((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))) *' ((((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))) + (1_ (17,F_Real)))) c= 17 \ 8 by A69, Th79;
hence vars R c= 17 \ 8 by A68, Th78; :: thesis: verum

end;

A72: for x being Function of 17,F_Real holds eval (R,x) = ((((eval (H,x)) - (eval (C,x))) * (eval (L,x))) + (((eval (F,x)) * ((x /. 9) + (1. F_Real))) * (eval (Q,x)))) + (((eval (F,x)) * ((x /. 8) + (1. F_Real))) * (((((((eval (W,x)) ^2) - (1. F_Real)) * (eval (S,x))) * (x /. 13)) - (((eval (W,x)) ^2) * ((x /. 13) ^2))) + (1. F_Real)))

proof

let x be Function of 17,F_Real; :: thesis: eval (R,x) = ((((eval (H,x)) - (eval (C,x))) * (eval (L,x))) + (((eval (F,x)) * ((x /. 9) + (1. F_Real))) * (eval (Q,x)))) + (((eval (F,x)) * ((x /. 8) + (1. F_Real))) * (((((((eval (W,x)) ^2) - (1. F_Real)) * (eval (S,x))) * (x /. 13)) - (((eval (W,x)) ^2) * ((x /. 13) ^2))) + (1. F_Real)))
A73: eval (((H - C) *' L),x) = (eval ((H - C),x)) * (eval (L,x)) by POLYNOM2:25
.= ((eval (H,x)) - (eval (C,x))) * (eval (L,x)) by POLYNOM2:24 ;
A74: eval (((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) + (1_ (17,F_Real)))) *' Q),x) = (eval ((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) + (1_ (17,F_Real)))),x)) * (eval (Q,x)) by POLYNOM2:25
.= ((eval (F,x)) * (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) + (1_ (17,F_Real))),x))) * (eval (Q,x)) by POLYNOM2:25
.= ((eval (F,x)) * ((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x)) + (eval ((1_ (17,F_Real)),x)))) * (eval (Q,x)) by POLYNOM2:23
.= ((eval (F,x)) * ((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x)) + (1. F_Real))) * (eval (Q,x)) by POLYNOM2:21
.= ((eval (F,x)) * ((x /. 9) + (1. F_Real))) * (eval (Q,x)) by A5 ;
A75: eval ((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))),x) = (eval (F,x)) * (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real))),x)) by POLYNOM2:25
.= (eval (F,x)) * ((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x)) + (eval ((1_ (17,F_Real)),x))) by POLYNOM2:23
.= (eval (F,x)) * ((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))),x)) + (1. F_Real)) by POLYNOM2:21
.= (eval (F,x)) * ((x /. 8) + (1. F_Real)) by A3 ;
A76: ( eval ((W *' W),x) = (eval (W,x)) * (eval (W,x)) & (eval (W,x)) * (eval (W,x)) = (eval (W,x)) ^2 ) by POLYNOM2:25, SQUARE_1:def 1;
then eval (((W *' W) - (1_ (17,F_Real))),x) = ((eval (W,x)) * (eval (W,x))) - (eval ((1_ (17,F_Real)),x)) by POLYNOM2:24;
then eval ((((W *' W) - (1_ (17,F_Real))) *' S),x) = (((eval (W,x)) * (eval (W,x))) - (eval ((1_ (17,F_Real)),x))) * (eval (S,x)) by POLYNOM2:25;
then A77: ( eval (((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))),x) = ((((eval (W,x)) * (eval (W,x))) - (eval ((1_ (17,F_Real)),x))) * (eval (S,x))) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x)) & eval ((1_ (17,F_Real)),x) = 1. F_Real & eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x) = x /. 13 ) by A13, POLYNOM2:21, POLYNOM2:25;
A78: eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x) = x /. 13 by A13;
A79: eval (((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))))),x) = (eval ((W *' W),x)) * (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))),x)) by POLYNOM2:25
.= (eval ((W *' W),x)) * ((x /. 13) * (x /. 13)) by A78, POLYNOM2:25
.= ((eval (W,x)) * (eval (W,x))) * ((x /. 13) * (x /. 13)) by POLYNOM2:25 ;
A80: eval (((((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))) + (1_ (17,F_Real))),x) = (eval ((((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval ((((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))),x)) + (1. F_Real) by POLYNOM2:21
.= ((eval (((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))),x)) - (eval (((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))))),x))) + (1. F_Real) by POLYNOM2:24
.= ((((((eval (W,x)) ^2) - (1. F_Real)) * (eval (S,x))) * (x /. 13)) - (((eval (W,x)) * (eval (W,x))) * ((x /. 13) * (x /. 13)))) + (1. F_Real) by A77, A79, SQUARE_1:def 1 ;
A81: eval (((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))) *' ((((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))) + (1_ (17,F_Real)))),x) = (eval ((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))),x)) * (eval (((((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))) + (1_ (17,F_Real))),x)) by POLYNOM2:25
.= ((eval (F,x)) * ((x /. 8) + (1. F_Real))) * (((((((eval (W,x)) ^2) - (1. F_Real)) * (eval (S,x))) * (x /. 13)) - (((eval (W,x)) ^2) * ((x /. 13) ^2))) + (1. F_Real)) by A76, A80, A75, SQUARE_1:def 1 ;
eval (R,x) = (eval ((((H - C) *' L) + ((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) + (1_ (17,F_Real)))) *' Q)),x)) + (eval (((F *' ((Monom ((1. F_Real),((EmptyBag 17) +* (8,1)))) + (1_ (17,F_Real)))) *' ((((((W *' W) - (1_ (17,F_Real))) *' S) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) - ((W *' W) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))))) + (1_ (17,F_Real)))),x)) by POLYNOM2:23;
hence eval (R,x) = ((((eval (H,x)) - (eval (C,x))) * (eval (L,x))) + (((eval (F,x)) * ((x /. 9) + (1. F_Real))) * (eval (Q,x)))) + (((eval (F,x)) * ((x /. 8) + (1. F_Real))) * (((((((eval (W,x)) ^2) - (1. F_Real)) * (eval (S,x))) * (x /. 13)) - (((eval (W,x)) ^2) * ((x /. 13) ^2))) + (1. F_Real))) by A81, A73, A74, POLYNOM2:23; :: thesis: verum

end;

reconsider Eight = 8 as integer Element of F_Real by XREAL_0:def 1;
reconsider V1 = Eight * (((((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' S) *' T) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U))) as INT -valued Polynomial of 17,F_Real ;
A82: vars V1 c= 17 \ 8

proof

vars ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) c= 17 \ 8 by A4, A12, Th79;
then vars (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' S) c= 17 \ 8 by A30, Th79;
then A83: vars ((((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' S) *' T) c= 17 \ 8 by A32, Th79;
vars ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) c= 17 \ 8 by A10, A30, Th79;
then vars (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) c= 17 \ 8 by A32, Th79;
then vars ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U) c= 17 \ 8 by A23, Th79;
then vars ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)) c= 17 \ 8 by A14, Th81;
then vars (((((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' S) *' T) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U))) c= 17 \ 8 by A83, Th79;
hence vars V1 c= 17 \ 8 by Th80; :: thesis: verum

end;

A84: for x being Function of 17,F_Real holds eval (V1,x) = Eight * (((((x /. 9) * (x /. 13)) * (eval (S,x))) * (eval (T,x))) * ((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)))))

proof

let x be Function of 17,F_Real; :: thesis: eval (V1,x) = Eight * (((((x /. 9) * (x /. 13)) * (eval (S,x))) * (eval (T,x))) * ((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)))))
eval (((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U),x) = (eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T),x)) * (eval (U,x)) by POLYNOM2:25
.= ((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S),x)) * (eval (T,x))) * (eval (U,x)) by POLYNOM2:25
.= (((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))),x)) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)) by POLYNOM2:25
.= (((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)) by A11 ;
then A85: eval (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)),x) = (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))),x)) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x))) by POLYNOM2:24
.= (x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x))) by A15 ;
eval (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))),x) = (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x)) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x)) by POLYNOM2:25
.= (x /. 9) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x)) by A5
.= (x /. 9) * (x /. 13) by A13 ;
then eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' S),x) = ((x /. 9) * (x /. 13)) * (eval (S,x)) by POLYNOM2:25;
then eval (((((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' S) *' T),x) = (((x /. 9) * (x /. 13)) * (eval (S,x))) * (eval (T,x)) by POLYNOM2:25;
then eval ((((((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' S) *' T) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U))),x) = ((((x /. 9) * (x /. 13)) * (eval (S,x))) * (eval (T,x))) * ((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)))) by A85, POLYNOM2:25;
hence eval (V1,x) = Eight * (((((x /. 9) * (x /. 13)) * (eval (S,x))) * (eval (T,x))) * ((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x))))) by POLYNOM7:29; :: thesis: verum

end;

reconsider Four = 4 as integer Element of F_Real by XREAL_0:def 1;
reconsider V2 = Four * ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (S *' S)) *' (T *' T)) as INT -valued Polynomial of 17,F_Real ;
A86: vars V2 c= 17 \ 8

proof

( vars ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) c= 17 \ 8 & vars (S *' S) c= 17 \ 8 ) by A30, A12, Th79;
then ( vars (((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (S *' S)) c= 17 \ 8 & vars (T *' T) c= 17 \ 8 ) by A32, Th79;
then vars ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (S *' S)) *' (T *' T)) c= 17 \ 8 by Th79;
hence vars V2 c= 17 \ 8 by Th80; :: thesis: verum

end;

A87: for x being Function of 17,F_Real holds eval (V2,x) = ((Four * ((x /. 13) ^2)) * ((eval (S,x)) ^2)) * ((eval (T,x)) ^2)

proof

let x be Function of 17,F_Real; :: thesis: eval (V2,x) = ((Four * ((x /. 13) ^2)) * ((eval (S,x)) ^2)) * ((eval (T,x)) ^2)
A88: ( eval (((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))),x) = (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x)) * (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x)) & eval ((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))),x) = x /. 13 ) by POLYNOM2:25, A13;
A89: ( eval ((S *' S),x) = (eval (S,x)) * (eval (S,x)) & eval ((T *' T),x) = (eval (T,x)) * (eval (T,x)) ) by POLYNOM2:25;
then eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (S *' S)),x) = ((x /. 13) * (x /. 13)) * ((eval (S,x)) * (eval (S,x))) by A88, POLYNOM2:25;
then A90: eval (((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (S *' S)) *' (T *' T)),x) = (((x /. 13) * (x /. 13)) * ((eval (S,x)) * (eval (S,x)))) * ((eval (T,x)) * (eval (T,x))) by A89, POLYNOM2:25;
thus eval (V2,x) = Four * (eval (((((Monom ((1. F_Real),((EmptyBag 17) +* (13,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (13,1))))) *' (S *' S)) *' (T *' T)),x)) by POLYNOM7:29
.= ((Four * ((x /. 13) * (x /. 13))) * ((eval (S,x)) * (eval (S,x)))) * ((eval (T,x)) * (eval (T,x))) by A90
.= ((Four * ((x /. 13) ^2)) * ((eval (S,x)) * (eval (S,x)))) * ((eval (T,x)) * (eval (T,x))) by SQUARE_1:def 1
.= ((Four * ((x /. 13) ^2)) * ((eval (S,x)) ^2)) * ((eval (T,x)) * (eval (T,x))) by SQUARE_1:def 1
.= ((Four * ((x /. 13) ^2)) * ((eval (S,x)) ^2)) * ((eval (T,x)) ^2) by SQUARE_1:def 1 ; :: thesis: verum

end;

reconsider V3 = ((Four * ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))))) - (1_ (17,F_Real))) *' (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U))) as INT -valued Polynomial of 17,F_Real ;
A91: vars V3 c= 17 \ 8

proof

vars ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) c= 17 \ 8 by A10, A30, Th79;
then vars (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) c= 17 \ 8 by A32, Th79;
then vars ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U) c= 17 \ 8 by A23, Th79;
then vars ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)) c= 17 \ 8 by A14, Th81;
then A92: vars (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U))) c= 17 \ 8 by Th79;
vars ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (9,1))))) c= 17 \ 8 by A4, Th79;
then vars (Four * ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))))) c= 17 \ 8 by Th80;
then vars ((Four * ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))))) - (1_ (17,F_Real))) c= 17 \ 8 by A20, Th81;
hence vars V3 c= 17 \ 8 by A92, Th79; :: thesis: verum

end;

A93: for x being Function of 17,F_Real holds eval (V3,x) = ((Four * ((x /. 9) ^2)) - (1. F_Real)) * (((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)))) ^2)

proof

let x be Function of 17,F_Real; :: thesis: eval (V3,x) = ((Four * ((x /. 9) ^2)) - (1. F_Real)) * (((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)))) ^2)
eval (((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U),x) = (eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T),x)) * (eval (U,x)) by POLYNOM2:25
.= ((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S),x)) * (eval (T,x))) * (eval (U,x)) by POLYNOM2:25
.= (((eval ((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))),x)) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)) by POLYNOM2:25
.= (((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)) by A11 ;
then A94: eval (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)),x) = (eval ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))),x)) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x))) by POLYNOM2:24
.= (x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x))) by A15 ;
eval ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))),x) = x /. 9 by A5;
then eval (((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (9,1))))),x) = (x /. 9) * (x /. 9) by POLYNOM2:25;
then eval ((Four * ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))))),x) = Four * ((x /. 9) * (x /. 9)) by POLYNOM7:29;
then A95: eval (((Four * ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))))) - (1_ (17,F_Real))),x) = (Four * ((x /. 9) * (x /. 9))) - (eval ((1_ (17,F_Real)),x)) by POLYNOM2:24
.= (Four * ((x /. 9) * (x /. 9))) - (1. F_Real) by POLYNOM2:21
.= (Four * ((x /. 9) ^2)) - (1. F_Real) by SQUARE_1:def 1 ;
eval ((((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)) *' ((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U))),x) = (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)),x)) * (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)),x)) by POLYNOM2:25;
then eval (V3,x) = (eval (((Four * ((Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))) *' (Monom ((1. F_Real),((EmptyBag 17) +* (9,1)))))) - (1_ (17,F_Real))),x)) * ((eval (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)),x)) * (eval (((Monom ((1. F_Real),((EmptyBag 17) +* (14,1)))) - ((((Monom ((1. F_Real),((EmptyBag 17) +* (12,1)))) *' S) *' T) *' U)),x))) by POLYNOM2:25
.= ((Four * ((x /. 9) ^2)) - (1. F_Real)) * (((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)))) * ((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x))))) by A95, A94 ;
hence eval (V3,x) = ((Four * ((x /. 9) ^2)) - (1. F_Real)) * (((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)))) ^2) by SQUARE_1:def 1; :: thesis: verum

end;

reconsider N1 = (M *' S) + (Two * ((M *' U) *' T)) as INT -valued Polynomial of 17,F_Real ;
A96: vars N1 c= 17 \ 8

proof

A97: vars (M *' S) c= 17 \ 8 by A28, A30, Th79;
vars (M *' U) c= 17 \ 8 by A28, A23, Th79;
then vars ((M *' U) *' T) c= 17 \ 8 by A32, Th79;
then vars (Two * ((M *' U) *' T)) c= 17 \ 8 by Th80;
hence vars N1 c= 17 \ 8 by A97, Th78; :: thesis: verum

end;

A98: for x being Function of 17,F_Real holds eval (N1,x) = ((eval (M,x)) * (eval (S,x))) + (((Two * (eval (M,x))) * (eval (U,x))) * (eval (T,x)))

proof

let x be Function of 17,F_Real; :: thesis: eval (N1,x) = ((eval (M,x)) * (eval (S,x))) + (((Two * (eval (M,x))) * (eval (U,x))) * (eval (T,x)))
A99: eval ((M *' S),x) = (eval (M,x)) * (eval (S,x)) by POLYNOM2:25;
eval ((M *' U),x) = (eval (M,x)) * (eval (U,x)) by POLYNOM2:25;
then eval (((M *' U) *' T),x) = ((eval (M,x)) * (eval (U,x))) * (eval (T,x)) by POLYNOM2:25;
then eval ((Two * ((M *' U) *' T)),x) = Two * (((eval (M,x)) * (eval (U,x))) * (eval (T,x))) by POLYNOM7:29;
hence eval (N1,x) = ((eval (M,x)) * (eval (S,x))) + (((Two * (eval (M,x))) * (eval (U,x))) * (eval (T,x))) by A99, POLYNOM2:23; :: thesis: verum

end;

reconsider N2 = Four * (((((A *' A) *' C) *' E) *' G) *' H) as INT -valued Polynomial of 17,F_Real ;
A100: vars N2 c= 17 \ 8

proof

vars (A *' A) c= 17 \ 8 by A38, Th79;
then vars ((A *' A) *' C) c= 17 \ 8 by A42, Th79;
then vars (((A *' A) *' C) *' E) c= 17 \ 8 by A46, Th79;
then vars ((((A *' A) *' C) *' E) *' G) c= 17 \ 8 by A51, Th79;
then vars (((((A *' A) *' C) *' E) *' G) *' H) c= 17 \ 8 by A53, Th79;
hence vars N2 c= 17 \ 8 by Th80; :: thesis: verum

end;

A101: for x being Function of 17,F_Real holds eval (N2,x) = Four * ((((((eval (A,x)) * (eval (A,x))) * (eval (C,x))) * (eval (E,x))) * (eval (G,x))) * (eval (H,x)))

proof

let x be Function of 17,F_Real; :: thesis: eval (N2,x) = Four * ((((((eval (A,x)) * (eval (A,x))) * (eval (C,x))) * (eval (E,x))) * (eval (G,x))) * (eval (H,x)))
eval ((((((A *' A) *' C) *' E) *' G) *' H),x) = (eval (((((A *' A) *' C) *' E) *' G),x)) * (eval (H,x)) by POLYNOM2:25
.= ((eval ((((A *' A) *' C) *' E),x)) * (eval (G,x))) * (eval (H,x)) by POLYNOM2:25
.= (((eval (((A *' A) *' C),x)) * (eval (E,x))) * (eval (G,x))) * (eval (H,x)) by POLYNOM2:25
.= ((((eval ((A *' A),x)) * (eval (C,x))) * (eval (E,x))) * (eval (G,x))) * (eval (H,x)) by POLYNOM2:25
.= (((((eval (A,x)) * (eval (A,x))) * (eval (C,x))) * (eval (E,x))) * (eval (G,x))) * (eval (H,x)) by POLYNOM2:25 ;
hence eval (N2,x) = Four * ((((((eval (A,x)) * (eval (A,x))) * (eval (C,x))) * (eval (E,x))) * (eval (G,x))) * (eval (H,x))) by POLYNOM7:29; :: thesis: verum

end;

reconsider V = ((V1 - V2) - V3) - (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
reconsider NN = ((N1 + N2) + R) + (1_ (17,F_Real)) as INT -valued Polynomial of 17,F_Real ;
A102: vars V c= 17 \ 8

proof

vars (V1 - V2) c= 17 \ 8 by A82, A86, Th81;
then vars ((V1 - V2) - V3) c= 17 \ 8 by A91, Th81;
hence vars V c= 17 \ 8 by A20, Th81; :: thesis: verum

end;

A103: vars NN c= 17 \ 8

proof

vars (N1 + N2) c= 17 \ 8 by A96, A100, Th78;
then vars ((N1 + N2) + R) c= 17 \ 8 by A66, Th78;
hence vars NN c= 17 \ 8 by A20, Th78; :: thesis: verum

end;

A104: for x being Function of 17,F_Real st x /. 8 is positive Nat & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat holds
( eval (X1,x) is odd Nat & eval (X2,x) is odd Nat & eval (X3,x) is Nat & eval (P,x) is positive Nat & eval (R,x) is Nat & eval (NN,x) is Nat & eval (NN,x) > (((sqrt (eval (X1,x))) + (2 * (sqrt (eval (X2,x))))) + (4 * (sqrt (eval (X3,x))))) + (eval (R,x)) )

proof

let x be Function of 17,F_Real; :: thesis: ( x /. 8 is positive Nat & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat implies ( eval (X1,x) is odd Nat & eval (X2,x) is odd Nat & eval (X3,x) is Nat & eval (P,x) is positive Nat & eval (R,x) is Nat & eval (NN,x) is Nat & eval (NN,x) > (((sqrt (eval (X1,x))) + (2 * (sqrt (eval (X2,x))))) + (4 * (sqrt (eval (X3,x))))) + (eval (R,x)) ) )
assume A105: ( x /. 8 is positive Nat & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat ) ; :: thesis: ( eval (X1,x) is odd Nat & eval (X2,x) is odd Nat & eval (X3,x) is Nat & eval (P,x) is positive Nat & eval (R,x) is Nat & eval (NN,x) is Nat & eval (NN,x) > (((sqrt (eval (X1,x))) + (2 * (sqrt (eval (X2,x))))) + (4 * (sqrt (eval (X3,x))))) + (eval (R,x)) )
reconsider xk = x /. 8, xf = x /. 9, xi = x /. 10, xj = x /. 11, xm = x /. 12, xu = x /. 13 as positive Nat by A105;
reconsider xr = x /. 14, xs = x /. 15, xt = x /. 16 as Nat by A105;
A106: eval (W,x) = ((Hund * (x /. 9)) * (x /. 8)) * ((x /. 8) + (1. F_Real)) by A22;
then A107: eval (W,x) = ((Hund * xf) * xk) * (xk + (1. F_Real)) ;
then reconsider eW = eval (W,x) as Element of NAT by INT_1:3;
A108: eval (U,x) = ((Hund * (xu |^ 3)) * (eW |^ 3)) + (1. F_Real) by A24;
then reconsider eU = eval (U,x) as positive Nat ;
A109: eval (M,x) = (((Hund * (x /. 12)) * (eval (U,x))) * (eval (W,x))) + (1. F_Real) by A29;
then eval (M,x) = (((Hund * xm) * eU) * eW) + (1. F_Real) ;
then reconsider eM = eval (M,x) as positive Nat ;
eval (S,x) = ((((eval (M,x)) - (1. F_Real)) * (x /. 15)) + (x /. 8)) + (1. F_Real) by A31;
then A110: eval (S,x) = (((eM - (1. F_Real)) * xs) + xk) + (1. F_Real) ;
then reconsider eS = eval (S,x) as Element of NAT by INT_1:3;
A111: eval (T,x) = ((((((eval (M,x)) * (eval (U,x))) - (1. F_Real)) * (x /. 16)) + (eval (W,x))) - (x /. 8)) + (1. F_Real) by A33;
A112: ((100 * xf) * xk) * (xk + 1) >= 1 * (xk + 1) by NAT_1:14, XREAL_1:64;
eW > xk by A112, A106, NAT_1:13;
then eW - xk > 0 by XREAL_1:50;
then (((eM * eU) - 1) * xt) + (eW - xk) >= 0 + 0 ;
then reconsider eT = eval (T,x) as Element of NAT by A111, INT_1:3;
A113: eval (Q,x) = (((Two * (eval (M,x))) * (eval (W,x))) - ((eval (W,x)) ^2)) - (1. F_Real) by A35;
(((Hund * xm) * eU) * eW) + 1 > 0 + 1 by A107, XREAL_1:6;
then ( eM >= 1 + 1 & eW >= 1 ) by A107, A109, NAT_1:8;
then eM * eW >= (1 + 1) * 1 by XREAL_1:66;
then A114: (eM * eW) - 1 >= 1 by XREAL_1:19;
((100 * xm) * eU) * eW >= 1 * eW by XREAL_1:64, NAT_1:14;
then eM > eW by A109, NAT_1:13;
then A115: ( eM * eW > eW * eW & eW * eW = eW ^2 ) by A107, XREAL_1:68, SQUARE_1:def 1;
then A116: (eM * eW) + (eM * eW) > (eM * eW) + (eW ^2) by XREAL_1:8;
then ((eM * eW) + (eM * eW)) - ((eW ^2) + 1) > ((eM * eW) + (eW ^2)) - ((eW ^2) + 1) by XREAL_1:9;
then reconsider eQ = eval (Q,x) as positive Nat by A113, A114;
eval (L,x) = ((x /. 8) + (1. F_Real)) * (eval (Q,x)) by A37;
then eval (L,x) = (xk + (1. F_Real)) * eQ ;
then reconsider eL = eval (L,x) as positive Nat ;
A117: eval (A,x) = (eval (M,x)) * ((eval (U,x)) + (1. F_Real)) by A39;
then A118: eval (A,x) = eM * (eU + (1. F_Real)) ;
( eM >= 1 & eU + 1 >= 1 + 1 ) by XREAL_1:6, NAT_1:14;
then A119: eM * (eU + (1. F_Real)) >= 1 * 2 by XREAL_1:66;
reconsider eA = eval (A,x) as positive Nat by A118;
eval (B,x) = (eval (W,x)) + (1. F_Real) by A41;
then eval (B,x) = eW + (1. F_Real) ;
then reconsider eB = eval (B,x) as positive Nat ;
eval (C,x) = ((x /. 14) + (eval (W,x))) + (1. F_Real) by A43;
then eval (C,x) = (xr + eW) + (1. F_Real) ;
then reconsider eC = eval (C,x) as positive Nat ;
A120: eval (D,x) = (((eA ^2) - (1. F_Real)) * (eC ^2)) + (1. F_Real) by A45;
A121: ( eA ^2 = eA * eA & eA * eA <> 0 ) by SQUARE_1:def 1;
reconsider eD = eval (D,x) as positive Nat by A121, A120;
A122: eval (E,x) = (((Two * (x /. 10)) * ((eval (C,x)) ^2)) * (eval (L,x))) * (eval (D,x)) by A47;
then A123: eval (E,x) = (((Two * xi) * (eC ^2)) * eL) * eD ;
A124: eC * eC = eC ^2 by SQUARE_1:def 1;
then reconsider eE = eval (E,x) as positive Nat by A123;
A125: eval (F,x) = (((eA ^2) - (1. F_Real)) * (eE ^2)) + (1. F_Real) by A50;
reconsider eF = eval (F,x) as positive Nat by A121, A125;
A126: eval (G,x) = (eval (A,x)) + ((eval (F,x)) * ((eval (F,x)) - (eval (A,x)))) by A52;
A127: ( eE ^2 = eE * eE & eE * eE >= 1 ) by NAT_1:14, SQUARE_1:def 1;
eA - 1 >= 2 - 1 by A117, A119, XREAL_1:9;
then A128: (eA - 1) * (eA + 1) >= 1 * (eA + 1) by XREAL_1:64;
then ((eA - 1) * (eA + 1)) * (eE ^2) >= (1 * (eA + 1)) * 1 by A127, XREAL_1:66;
then (((eA - 1) * (eA + 1)) * (eE ^2)) + 1 >= (eA + 1) + 0 by XREAL_1:7;
then eF > eA by A121, A125, NAT_1:13;
then eF - eA > eA - eA by XREAL_1:14;
then reconsider eG = eval (G,x) as positive Nat by A126;
eval (H,x) = (eval (B,x)) + ((Two * ((x /. 11) - (1. F_Real))) * (eval (C,x))) by A54;
then A129: eval (H,x) = eB + ((Two * (xj - (1. F_Real))) * eC) ;
reconsider eH = eval (H,x) as positive Nat by A129;
A130: eval (I,x) = (((eG ^2) - (1. F_Real)) * (eH ^2)) + (1. F_Real) by A56;
( eG ^2 = eG * eG & eG * eG <> 0 ) by SQUARE_1:def 1;
then reconsider eI = eval (I,x) as positive Nat by A130;
A131: eval (X1,x) = (((eM ^2) - (1. F_Real)) * (eS ^2)) + (1. F_Real) by A58;
A132: ( eM ^2 = eM * eM & eM * eM <> 0 ) by SQUARE_1:def 1;
then reconsider eX1 = eval (X1,x) as Nat by A131;
A133: eM = (2 * (((50 * xm) * eU) * eW)) + 1 by A109;
hence eval (X1,x) is odd Nat by A132, A131; :: thesis: ( eval (X2,x) is odd Nat & eval (X3,x) is Nat & eval (P,x) is positive Nat & eval (R,x) is Nat & eval (NN,x) is Nat & eval (NN,x) > (((sqrt (eval (X1,x))) + (2 * (sqrt (eval (X2,x))))) + (4 * (sqrt (eval (X3,x))))) + (eval (R,x)) )
A134: eval (X2,x) = (((((eval (M,x)) * (eval (U,x))) ^2) - (1. F_Real)) * ((eval (T,x)) ^2)) + (1. F_Real) by A60;
then A135: eval (X2,x) = ((((eM * eU) ^2) - (1. F_Real)) * (eT ^2)) + (1. F_Real) ;
A136: ( (eM * eU) ^2 = (eM * eU) * (eM * eU) & (eM * eU) * (eM * eU) <> 0 ) by SQUARE_1:def 1;
then reconsider eX2 = eval (X2,x) as Nat by A135;
eU = (2 * ((50 * (xu |^ 3)) * (eW |^ 3))) + (1. F_Real) by A108;
hence eval (X2,x) is odd Nat by A133, A136, A135; :: thesis: ( eval (X3,x) is Nat & eval (P,x) is positive Nat & eval (R,x) is Nat & eval (NN,x) is Nat & eval (NN,x) > (((sqrt (eval (X1,x))) + (2 * (sqrt (eval (X2,x))))) + (4 * (sqrt (eval (X3,x))))) + (eval (R,x)) )
A137: eval (X3,x) = ((eval (D,x)) * (eval (F,x))) * (eval (I,x)) by A63;
then A138: eval (X3,x) = (eD * eF) * eI ;
then reconsider eX3 = eval (X3,x) as Nat ;
thus eval (X3,x) is Nat by A138; :: thesis: ( eval (P,x) is positive Nat & eval (R,x) is Nat & eval (NN,x) is Nat & eval (NN,x) > (((sqrt (eval (X1,x))) + (2 * (sqrt (eval (X2,x))))) + (4 * (sqrt (eval (X3,x))))) + (eval (R,x)) )
eval (P,x) = (eval (F,x)) * (eval (L,x)) by A65;
then eval (P,x) = eF * eL ;
hence eval (P,x) is positive Nat ; :: thesis: ( eval (R,x) is Nat & eval (NN,x) is Nat & eval (NN,x) > (((sqrt (eval (X1,x))) + (2 * (sqrt (eval (X2,x))))) + (4 * (sqrt (eval (X3,x))))) + (eval (R,x)) )
A139: eval (R,x) = ((((eval (H,x)) - (eval (C,x))) * (eval (L,x))) + (((eval (F,x)) * ((x /. 9) + (1. F_Real))) * (eval (Q,x)))) + (((eval (F,x)) * ((x /. 8) + (1. F_Real))) * (((((((eval (W,x)) ^2) - (1. F_Real)) * (eval (S,x))) * (x /. 13)) - (((eval (W,x)) ^2) * ((x /. 13) ^2))) + (1. F_Real))) by A72;
then eval (R,x) = (((eH - eC) * eL) + ((eF * (xf + 1)) * eQ)) + ((eF * (xk + 1)) * ((((((eW ^2) - 1) * eS) * xu) - ((eW ^2) * (xu ^2))) + 1)) ;
then reconsider eR = eval (R,x) as Integer ;
xk + 1 >= 1 by NAT_1:14;
then A140: eF * (xk + 1) >= eF * 1 by XREAL_1:66;
eE >= 1 by NAT_1:14;
then A141: ( eE ^2 = eE * eE & eE * eE >= eE * 1 ) by XREAL_1:66, SQUARE_1:def 1;
A142: eA * eA = eA ^2 by SQUARE_1:def 1;
(eA ^2) - 1 >= 1 by A142, A128, NAT_1:14;
then (((eA ^2) - 1) * (eE ^2)) + 1 > eE by NAT_1:13, A141, XREAL_1:66;
then A143: eF * (xk + 1) > eE by A125, A140, XXREAL_0:2;
((Two * xi) * eC) * eD >= 1 by NAT_1:14;
then (((Two * xi) * eC) * eD) * (eC * eL) >= 1 * (eC * eL) by XREAL_1:66;
then eF * (xk + 1) > eC * eL by A124, A143, A122, XXREAL_0:2;
then (eF * (xk + 1)) - (eC * eL) > 0 by XREAL_1:50;
then A144: ((eF * (xk + 1)) - (eC * eL)) + ((eH * eL) + ((((eF * (xk + 1)) * ((eW ^2) - 1)) * eS) * xu)) >= 0 + 0 by A107, A115;
(eM * eW) + (eM * eW) >= ((eM * eW) + (eW ^2)) + 1 by A116, NAT_1:13;
then A145: ((eM * eW) + (eM * eW)) - ((eW ^2) + 1) >= (((eM * eW) + (eW ^2)) + 1) - ((eW ^2) + 1) by XREAL_1:6;
(Hund * xf) * xk >= 1 by NAT_1:14;
then A146: eW >= (xk + 1) * 1 by A106, XREAL_1:66;
then eM * eW >= (xk + 1) * eM by XREAL_1:66;
then A147: eQ >= (xk + 1) * eM by A145, A113, XXREAL_0:2;
A148: xu >= 1 by NAT_1:14;
A149: 100 * xm >= 1 by NAT_1:14;
xu |^ (2 + 1) = (xu |^ 2) * xu by NEWTON:6
.= (xu ^2) * xu by NEWTON:81 ;
then A150: xu |^ 3 >= (xu ^2) * 1 by A148, XREAL_1:66;
eW >= 1 by A107, NAT_1:14;
then eW |^ 3 >= eW by PREPOWER:12;
then (xu |^ 3) * (eW |^ 3) >= (xu ^2) * eW by A150, XREAL_1:66;
then 100 * ((xu |^ 3) * (eW |^ 3)) >= 1 * ((xu ^2) * eW) by XREAL_1:66;
then eU > (xu ^2) * eW by A108, NAT_1:13;
then eU * eW >= ((xu ^2) * eW) * eW by XREAL_1:66;
then (100 * xm) * (eU * eW) >= 1 * (((xu ^2) * eW) * eW) by A149, XREAL_1:66;
then eM > ((xu ^2) * eW) * eW by A109, NAT_1:13;
then (xk + 1) * eM >= (xk + 1) * (((xu ^2) * eW) * eW) by XREAL_1:66;
then ( eQ >= (xk + 1) * (((xu ^2) * eW) * eW) & xf + 1 >= 1 ) by A147, XXREAL_0:2, NAT_1:14;
then (xf + 1) * eQ >= ((xk + 1) * (((xu ^2) * eW) * eW)) * 1 by XREAL_1:66;
then eF * ((xf + 1) * eQ) >= eF * (((xk + 1) * (eW ^2)) * (xu ^2)) by A115, XREAL_1:66;
then ((eF * (xf + 1)) * eQ) - (((eF * (xk + 1)) * (eW ^2)) * (xu ^2)) >= 0 by XREAL_1:48;
then A151: ((((eH - eC) * eL) + (eF * (xk + 1))) + ((((eF * (xk + 1)) * ((eW ^2) - 1)) * eS) * xu)) + (((eF * (xf + 1)) * eQ) - (((eF * (xk + 1)) * (eW ^2)) * (xu ^2))) >= 0 by A144;
hence eval (R,x) is Nat by A139; :: thesis: ( eval (NN,x) is Nat & eval (NN,x) > (((sqrt (eval (X1,x))) + (2 * (sqrt (eval (X2,x))))) + (4 * (sqrt (eval (X3,x))))) + (eval (R,x)) )
A152: eval (N1,x) = ((eval (M,x)) * (eval (S,x))) + (((Two * (eval (M,x))) * (eval (U,x))) * (eval (T,x))) by A98;
then eval (N1,x) = (eM * eS) + (((2 * eM) * eU) * eT) ;
then reconsider eN1 = eval (N1,x) as Nat ;
A153: eval (N2,x) = Four * ((((((eval (A,x)) * (eval (A,x))) * (eval (C,x))) * (eval (E,x))) * (eval (G,x))) * (eval (H,x))) by A101;
then eval (N2,x) = 4 * (((((eA * eA) * eC) * eE) * eH) * eG) ;
then reconsider eN2 = eval (N2,x) as Nat ;
eW - ((xk + 1) * 1) >= 0 by A146, XREAL_1:48;
then ((eW - xk) - 1) + 2 >= 0 + 2 by XREAL_1:6;
then (((eM * eU) - 1) * xt) + ((eW - xk) + 1) >= 0 + 2 by XREAL_1:7;
then A154: ( eT ^2 = eT * eT & eT * eT >= 1 ) by A111, NAT_1:14, SQUARE_1:def 1;
then (((eM * eU) ^2) * (eT ^2)) - ((eT ^2) - 1) <= (((eM * eU) ^2) * (eT ^2)) - 0 by XREAL_1:6;
then eX2 <= ((eM * eU) * eT) * ((eM * eU) * eT) by A134, A154, A136;
then eX2 <= ((eM * eU) * eT) ^2 by SQUARE_1:def 1;
then ( sqrt eX2 <= sqrt (((eM * eU) * eT) ^2) & sqrt (((eM * eU) * eT) ^2) = (eM * eU) * eT ) by SQUARE_1:22, SQUARE_1:26;
then A155: 2 * (sqrt eX2) <= 2 * ((eM * eU) * eT) by XREAL_1:64;
A156: ( eS ^2 = eS * eS & eS * eS >= 1 ) by A110, NAT_1:14, SQUARE_1:def 1;
then ((eM ^2) * (eS ^2)) - ((eS ^2) - 1) <= ((eM ^2) * (eS ^2)) - 0 by XREAL_1:6;
then A157: ( eX1 <= (eM ^2) * (eS ^2) & eM * eM = eM ^2 ) by A131, SQUARE_1:def 1;
eX1 <= (eM * eS) * (eM * eS) by A156, A157;
then eX1 <= (eM * eS) ^2 by SQUARE_1:def 1;
then ( sqrt eX1 <= sqrt ((eM * eS) ^2) & sqrt ((eM * eS) ^2) = eM * eS ) by SQUARE_1:22, SQUARE_1:26;
then A158: (sqrt eX1) + (2 * (sqrt eX2)) <= eN1 by A152, A155, XREAL_1:7;
( eC ^2 = eC * eC & eC * eC >= 1 ) by NAT_1:14, SQUARE_1:def 1;
then A159: ((eA ^2) * (eC ^2)) - ((eC ^2) - 1) <= ((eA ^2) * (eC ^2)) - 0 by XREAL_1:6;
A160: ( eE ^2 = eE * eE & eE * eE >= 1 ) by NAT_1:14, SQUARE_1:def 1;
then ((eA ^2) * (eE ^2)) - ((eE ^2) - 1) <= ((eA ^2) * (eE ^2)) - 0 by XREAL_1:6;
then A161: eD * eF <= ((eA ^2) * (eC ^2)) * ((eA ^2) * (eE ^2)) by A120, A125, A159, XREAL_1:66;
A162: ( eH ^2 = eH * eH & eH * eH >= 1 ) by NAT_1:14, SQUARE_1:def 1;
then ((eG ^2) * (eH ^2)) - ((eH ^2) - 1) <= ((eG ^2) * (eH ^2)) - 0 by XREAL_1:6;
then (eD * eF) * eI <= (((eA ^2) * (eC ^2)) * ((eA ^2) * (eE ^2))) * ((eG ^2) * (eH ^2)) by A130, A161, XREAL_1:66;
then eX3 <= (((eA * eA) * (eC * eC)) * ((eA * eA) * (eE * eE))) * ((eG * eG) * (eH * eH)) by A137, A124, A121, A162, A160, SQUARE_1:def 1;
then eX3 <= (((((eA * eA) * eC) * eE) * eH) * eG) * (((((eA * eA) * eC) * eE) * eH) * eG) ;
then eX3 <= (((((eA * eA) * eC) * eE) * eH) * eG) ^2 by SQUARE_1:def 1;
then ( sqrt eX3 <= sqrt ((((((eA * eA) * eC) * eE) * eH) * eG) ^2) & sqrt ((((((eA * eA) * eC) * eE) * eH) * eG) ^2) = ((((eA * eA) * eC) * eE) * eH) * eG ) by SQUARE_1:22, SQUARE_1:26;
then A163: 4 * (sqrt eX3) <= eN2 by A153, XREAL_1:64;
A164: eval (NN,x) = (eval (((N1 + N2) + R),x)) + (eval ((1_ (17,F_Real)),x)) by POLYNOM2:23
.= (eval (((N1 + N2) + R),x)) + (1. F_Real) by POLYNOM2:21
.= ((eval ((N1 + N2),x)) + (eval (R,x))) + (1. F_Real) by POLYNOM2:23
.= (((eval (N1,x)) + (eval (N2,x))) + (eval (R,x))) + (1. F_Real) by POLYNOM2:23
.= ((eN1 + eN2) + eR) + 1 ;
A165: ((eN1 + eN2) + eR) + 1 > ((eN1 + eN2) + eR) + 0 by XREAL_1:6;
eN1 + eN2 >= ((sqrt eX1) + (2 * (sqrt eX2))) + (4 * (sqrt eX3)) by A158, A163, XREAL_1:7;
then (eN1 + eN2) + eR >= (((sqrt eX1) + (2 * (sqrt eX2))) + (4 * (sqrt eX3))) + eR by XREAL_1:6;
hence ( eval (NN,x) is Nat & eval (NN,x) > (((sqrt (eval (X1,x))) + (2 * (sqrt (eval (X2,x))))) + (4 * (sqrt (eval (X3,x))))) + (eval (R,x)) ) by A151, A139, A164, A165, XXREAL_0:2; :: thesis: verum

end;

consider K3 being INT -valued Polynomial of 8,F_Real such that
A166: for x1, x2, x3, P, R, N being Nat
for V being Integer st x1 is odd & x2 is odd & P > 0 & N > (((sqrt x1) + (2 * (sqrt x2))) + (4 * (sqrt x3))) + R holds
( ( x1 is square & x2 is square & x3 is square & P divides R & V >= 0 ) iff ex z being Nat st
for f being Function of 8,F_Real st f = <%z,x1,(4 * x2),(16 * x3)%> ^ <%R,P,N,V%> holds
eval (K3,f) = 0 ) by Th77;
consider Z being Polynomial of (8 + 9),F_Real such that
A167: rng Z c= (rng K3) \/ {(0. F_Real)} and
A168: for b being bag of 8 + 9 holds
( b in Support Z iff ( b | 8 in Support K3 & ( for i being Nat st i >= 8 holds
b . i = 0 ) ) ) and
for b being bag of 8 + 9 st b in Support Z holds
Z . b = K3 . (b | 8) and
A169: for x being Function of 8,F_Real
for y being Function of (8 + 9),F_Real st y | 8 = x holds
eval (K3,x) = eval (Z,y) by Th75;
rng Z c= INT by A167, INT_1:def 2;
then reconsider Z = Z as INT -valued Polynomial of 17,F_Real by RELAT_1:def 19;
reconsider Z1 = Subst (Z,1,X1) as INT -valued Polynomial of 17,F_Real ;
reconsider Z2 = Subst (Z1,2,(Four * X2)) as INT -valued Polynomial of 17,F_Real ;
reconsider Z3 = Subst (Z2,3,((Four * Four) * X3)) as INT -valued Polynomial of 17,F_Real ;
reconsider Z4 = Subst (Z3,4,R) as INT -valued Polynomial of 17,F_Real ;
reconsider Z5 = Subst (Z4,5,P) as INT -valued Polynomial of 17,F_Real ;
reconsider Z6 = Subst (Z5,6,NN) as INT -valued Polynomial of 17,F_Real ;
reconsider Z7 = Subst (Z6,7,V) as INT -valued Polynomial of 17,F_Real ;
take Z7 ; :: thesis: ( vars Z7 c= {0} \/ (17 \ 8) & ( for xk being Nat st xk > 0 holds
( xk + 1 is prime iff ex x being INT -valued Function of 17,F_Real st
( x /. 8 = xk & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) ) ) )
A170: for xk being Nat st xk > 0 holds
( xk + 1 is prime iff ex x being INT -valued Function of 17,F_Real st
( x /. 8 = xk & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) )

proof

let k1 be Nat; :: thesis: ( k1 > 0 implies ( k1 + 1 is prime iff ex x being INT -valued Function of 17,F_Real st
( x /. 8 = k1 & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) ) )
assume A171: k1 > 0 ; :: thesis: ( k1 + 1 is prime iff ex x being INT -valued Function of 17,F_Real st
( x /. 8 = k1 & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) )
thus ( k1 + 1 is prime implies ex x being INT -valued Function of 17,F_Real st
( x /. 8 = k1 & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) ) :: thesis: ( ex x being INT -valued Function of 17,F_Real st
( x /. 8 = k1 & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) implies k1 + 1 is prime )

proof

assume k1 + 1 is prime ; :: thesis: ex x being INT -valued Function of 17,F_Real st
( x /. 8 = k1 & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real )
then consider f1, i1, j1, m1, u1 being positive Nat, r1, s1, t1 being Nat, A1, B1, C1, D1, E1, F1, G1, H1, I1, L1, W1, U1, M1, S1, T1, Q1 being Integer such that
A172: ( (D1 * F1) * I1 is square & (((M1 ^2) - 1) * (S1 ^2)) + 1 is square & ((((M1 * U1) ^2) - 1) * (T1 ^2)) + 1 is square ) and
A173: (((4 * (f1 ^2)) - 1) * ((r1 - (((m1 * S1) * T1) * U1)) ^2)) + (((4 * (u1 ^2)) * (S1 ^2)) * (T1 ^2)) < ((((8 * f1) * u1) * S1) * T1) * (r1 - (((m1 * S1) * T1) * U1)) and
A174: F1 * L1 divides (((H1 - C1) * L1) + ((F1 * (f1 + 1)) * Q1)) + ((F1 * (k1 + 1)) * ((((((W1 ^2) - 1) * S1) * u1) - ((W1 ^2) * (u1 ^2))) + 1)) and
A175: A1 = M1 * (U1 + 1) and
A176: B1 = W1 + 1 and
A177: C1 = (r1 + W1) + 1 and
A178: D1 = (((A1 ^2) - 1) * (C1 ^2)) + 1 and
A179: E1 = (((2 * i1) * (C1 ^2)) * L1) * D1 and
A180: F1 = (((A1 ^2) - 1) * (E1 ^2)) + 1 and
A181: G1 = A1 + (F1 * (F1 - A1)) and
A182: H1 = B1 + ((2 * (j1 - 1)) * C1) and
A183: I1 = (((G1 ^2) - 1) * (H1 ^2)) + 1 and
A184: L1 = (k1 + 1) * Q1 and
A185: W1 = ((100 * f1) * k1) * (k1 + 1) and
A186: U1 = ((100 * (u1 |^ 3)) * (W1 |^ 3)) + 1 and
A187: M1 = (((100 * m1) * U1) * W1) + 1 and
A188: S1 = (((M1 - 1) * s1) + k1) + 1 and
A189: T1 = (((((M1 * U1) - 1) * t1) + W1) - k1) + 1 and
A190: Q1 = (((2 * M1) * W1) - (W1 ^2)) - 1 by A171, HILB10_8:23;
set zz = ((((((<%0%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>;
set vv = (((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>;
set x = @ ((((((((<%0%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>));
reconsider x = @ ((((((((<%0%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) as INT -valued Function of 17,F_Real ;
A191: len (((((((<%0%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) = 8 by AFINSQ_1:49;
A192: ( len ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) = 9 & 9 = Segm 9 ) by AFINSQ_1:50;
A193: ( dom x = 17 & 17 = Segm 17 ) by FUNCT_2:def 1;
A194: ( 0 in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) & 1 in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) & 2 in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) & 3 in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) & 4 in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) & 5 in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) & 6 in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) & 7 in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) & 8 in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) ) by A192, NAT_1:44;
A195: x /. 8 = x . (8 + 0) by A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 0 by A194, A191, AFINSQ_1:def 3
.= k1 by AFINSQ_1:50 ;
A196: x /. 9 = x . (8 + 1) by A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 1 by A194, A191, AFINSQ_1:def 3
.= f1 by AFINSQ_1:50 ;
A197: x /. 10 = x . (8 + 2) by A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 2 by A194, A191, AFINSQ_1:def 3
.= i1 by AFINSQ_1:50 ;
A198: x /. 11 = x . (8 + 3) by A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 3 by A194, A191, AFINSQ_1:def 3
.= j1 by AFINSQ_1:50 ;
A199: x /. 12 = x . (8 + 4) by A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 4 by A194, A191, AFINSQ_1:def 3
.= m1 by AFINSQ_1:50 ;
A200: x /. 13 = x . (8 + 5) by A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 5 by A194, A191, AFINSQ_1:def 3
.= u1 by AFINSQ_1:50 ;
A201: x /. 14 = x . (8 + 6) by A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 6 by A194, A191, AFINSQ_1:def 3
.= r1 by AFINSQ_1:50 ;
A202: x /. 15 = x . (8 + 7) by A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 7 by A194, A191, AFINSQ_1:def 3
.= s1 by AFINSQ_1:50 ;
A203: x /. 16 = x . (8 + 8) by A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 8 by A194, A191, AFINSQ_1:def 3
.= t1 by AFINSQ_1:50 ;
A204: eval (W,x) = ((Hund * (x /. 9)) * (x /. 8)) * ((x /. 8) + (1. F_Real)) by A22;
A205: U1 = eval (U,x) by A186, A200, A204, A185, A195, A196, A24;
A206: eval (M,x) = (((Hund * (x /. 12)) * (eval (U,x))) * (eval (W,x))) + (1. F_Real) by A29;
then A207: M1 = eval (M,x) by A187, A199, A186, A200, A204, A185, A195, A196, A24;
A208: eval (S,x) = ((((eval (M,x)) - (1. F_Real)) * (x /. 15)) + (x /. 8)) + (1. F_Real) by A31;
then A209: S1 = eval (S,x) by A188, A202, A195, A206, A187, A199, A186, A200, A204, A185, A196, A24;
A210: eval (T,x) = ((((((eval (M,x)) * (eval (U,x))) - (1. F_Real)) * (x /. 16)) + (eval (W,x))) - (x /. 8)) + (1. F_Real) by A33;
A211: eval (Q,x) = (((Two * (eval (M,x))) * (eval (W,x))) - ((eval (W,x)) ^2)) - (1. F_Real) by A35;
then A212: Q1 = eval (Q,x) by A190, A206, A187, A199, A186, A200, A204, A185, A195, A196, A24;
A213: eval (L,x) = ((x /. 8) + (1. F_Real)) * (eval (Q,x)) by A37;
A214: eval (A,x) = (eval (M,x)) * ((eval (U,x)) + (1. F_Real)) by A39;
A215: eval (B,x) = (eval (W,x)) + (1. F_Real) by A41;
A216: eval (C,x) = ((x /. 14) + (eval (W,x))) + (1. F_Real) by A43;
A217: D1 = eval (D,x) by A45, A178, A214, A175, A206, A187, A199, A204, A185, A195, A196, A205, A216, A177, A201;
A218: eval (E,x) = (((Two * (x /. 10)) * ((eval (C,x)) ^2)) * (eval (L,x))) * (eval (D,x)) by A47;
A219: F1 = eval (F,x) by A50, A180, A214, A175, A206, A187, A199, A204, A185, A195, A196, A205, A218, A179, A197, A213, A184, A211, A190, A216, A177, A201, A217;
A220: eval (G,x) = (eval (A,x)) + ((eval (F,x)) * ((eval (F,x)) - (eval (A,x)))) by A52;
A221: eval (H,x) = (eval (B,x)) + ((Two * ((x /. 11) - (1. F_Real))) * (eval (C,x))) by A54;
A222: I1 = eval (I,x) by A56, A183, A220, A181, A214, A175, A206, A187, A199, A204, A185, A195, A196, A205, A219, A221, A182, A215, A176, A198, A216, A177, A201;
reconsider X11 = eval (X1,x), X21 = eval (X2,x) as odd Nat by A104, A171, A195, A196, A197, A198, A199, A200, A201, A202, A203;
reconsider X31 = eval (X3,x), R1 = eval (R,x), NN1 = eval (NN,x) as Nat by A171, A195, A196, A197, A198, A199, A200, A201, A202, A203, A104;
reconsider P1 = eval (P,x) as positive Nat by A171, A195, A196, A197, A198, A199, A200, A201, A202, A203, A104;
A223: X11 = (((M1 ^2) - 1) * (S1 ^2)) + 1 by A58, A208, A207, A188, A202, A195;
A224: X21 = ((((M1 * U1) ^2) - 1) * (T1 ^2)) + 1 by A60, A206, A205, A210, A189, A204, A185, A195, A196, A203, A187, A199;
A225: eval (X3,x) = ((eval (D,x)) * (eval (F,x))) * (eval (I,x)) by A63;
A226: eval (P,x) = (eval (F,x)) * (eval (L,x)) by A65;
A227: eval (R,x) = ((((eval (H,x)) - (eval (C,x))) * (eval (L,x))) + (((eval (F,x)) * ((x /. 9) + (1. F_Real))) * (eval (Q,x)))) + (((eval (F,x)) * ((x /. 8) + (1. F_Real))) * (((((((eval (W,x)) ^2) - (1. F_Real)) * (eval (S,x))) * (x /. 13)) - (((eval (W,x)) ^2) * ((x /. 13) ^2))) + (1. F_Real))) by A72;
reconsider V11 = eval (V1,x), V21 = eval (V2,x), V31 = eval (V3,x) as Integer ;
A228: eval (V1,x) = Eight * (((((x /. 9) * (x /. 13)) * (eval (S,x))) * (eval (T,x))) * ((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x))))) by A84;
A229: eval (V3,x) = ((Four * ((x /. 9) ^2)) - (1. F_Real)) * (((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)))) ^2) by A93;
reconsider VV = ((V11 - V21) - V31) - 1 as Integer ;
A230: NN1 > (((sqrt X11) + (2 * (sqrt X21))) + (4 * (sqrt X31))) + R1 by A171, A195, A196, A197, A198, A199, A200, A201, A202, A203, A104;
A231: eval (V,x) = (eval (((V1 - V2) - V3),x)) - (eval ((1_ (17,F_Real)),x)) by POLYNOM2:24
.= (eval (((V1 - V2) - V3),x)) - (1. F_Real) by POLYNOM2:21
.= ((eval ((V1 - V2),x)) - (eval (V3,x))) - (1. F_Real) by POLYNOM2:24
.= (((eval (V1,x)) - (eval (V2,x))) - (eval (V3,x))) - (1. F_Real) by POLYNOM2:24 ;
( V31 + V21 < V11 & VV + 1 = V11 - (V31 + V21) ) by A173, A228, A87, A200, A208, A210, A189, A206, A204, A185, A195, A196, A203, A187, A199, A229, A201, A205, A188, A202;
then A232: 0 < VV + 1 by XREAL_1:50;
consider z1 being Nat such that
A233: for f being Function of 8,F_Real st f = <%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%> holds
eval (K3,f) = 0 by A166, A230, A172, A223, A224, A225, A217, A213, A184, A195, A200, A204, A185, A196, A216, A177, A201, A222, A232, A174, A226, A227, A221, A182, A215, A198, A219, A212, A209, A176;
set yy = ((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>;
set p = @ ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>));
reconsider p = @ ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) as INT -valued Function of 17,F_Real ;
A234: 17 = Segm 17 ;
then A235: ( 0 in 17 & 1 in 17 & 2 in 17 & 3 in 17 & 4 in 17 & 5 in 17 & 6 in 17 & 7 in 17 ) by NAT_1:44;
set p7 = p +* (7,(eval (V,p)));
A236: eval (Z7,p) = eval (Z6,(p +* (7,(eval (V,p))))) by Th37, A234, NAT_1:44;
set p6 = (p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)));
not 7 in vars NN by A1, A103;
then 7 in 17 \ (vars NN) by A235, XBOOLE_0:def 5;
then eval (NN,(p +* (7,(eval (V,p))))) = eval (NN,p) by Th53;
then A237: eval (Z6,(p +* (7,(eval (V,p))))) = eval (Z5,((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p))))) by Th37, A234, NAT_1:44;
set p5 = ((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)));
( not 6 in vars P & not 7 in vars P ) by A64, A1;
then A238: ( 6 in 17 \ (vars P) & 7 in 17 \ (vars P) ) by A235, XBOOLE_0:def 5;
then eval (P,((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p))))) = eval (P,(p +* (7,(eval (V,p))))) by Th53
.= eval (P,p) by A238, Th53 ;
then A239: eval (Z5,((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p))))) = eval (Z4,(((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p))))) by Th37, A234, NAT_1:44;
set p4 = (((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)));
( not 5 in vars R & not 6 in vars R & not 7 in vars R ) by A66, A1;
then A240: ( 5 in 17 \ (vars R) & 6 in 17 \ (vars R) & 7 in 17 \ (vars R) ) by A235, XBOOLE_0:def 5;
then eval (R,(((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p))))) = eval (R,((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p))))) by Th53
.= eval (R,(p +* (7,(eval (V,p))))) by A240, Th53
.= eval (R,p) by A240, Th53 ;
then A241: eval (Z4,(((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p))))) = eval (Z3,((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p))))) by Th37, A234, NAT_1:44;
A242: vars ((Four * Four) * X3) c= 17 \ 8 by Th80, A62;
set p3 = ((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)));
( not 4 in vars ((Four * Four) * X3) & not 5 in vars ((Four * Four) * X3) & not 6 in vars ((Four * Four) * X3) & not 7 in vars ((Four * Four) * X3) ) by A1, A242;
then A243: ( 4 in 17 \ (vars ((Four * Four) * X3)) & 5 in 17 \ (vars ((Four * Four) * X3)) & 6 in 17 \ (vars ((Four * Four) * X3)) & 7 in 17 \ (vars ((Four * Four) * X3)) ) by A235, XBOOLE_0:def 5;
then eval (((Four * Four) * X3),((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p))))) = eval (((Four * Four) * X3),(((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p))))) by Th53
.= eval (((Four * Four) * X3),((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p))))) by A243, Th53
.= eval (((Four * Four) * X3),(p +* (7,(eval (V,p))))) by A243, Th53
.= eval (((Four * Four) * X3),p) by A243, Th53 ;
then A244: eval (Z3,((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p))))) = eval (Z2,(((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p))))) by Th37, A234, NAT_1:44;
A245: vars (Four * X2) c= 17 \ 8 by Th80, A59;
set p2 = (((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)));
( not 3 in vars (Four * X2) & not 4 in vars (Four * X2) & not 5 in vars (Four * X2) & not 6 in vars (Four * X2) & not 7 in vars (Four * X2) ) by A1, A245;
then A246: ( 3 in 17 \ (vars (Four * X2)) & 4 in 17 \ (vars (Four * X2)) & 5 in 17 \ (vars (Four * X2)) & 6 in 17 \ (vars (Four * X2)) & 7 in 17 \ (vars (Four * X2)) ) by A235, XBOOLE_0:def 5;
then eval ((Four * X2),(((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p))))) = eval ((Four * X2),((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p))))) by Th53
.= eval ((Four * X2),(((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p))))) by A246, Th53
.= eval ((Four * X2),((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p))))) by A246, Th53
.= eval ((Four * X2),(p +* (7,(eval (V,p))))) by A246, Th53
.= eval ((Four * X2),p) by A246, Th53 ;
then A247: eval (Z2,(((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p))))) = eval (Z1,((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p))))) by Th37, A234, NAT_1:44;
set p1 = ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)));
( not 2 in vars X1 & not 3 in vars X1 & not 4 in vars X1 & not 5 in vars X1 & not 6 in vars X1 & not 7 in vars X1 ) by A1, A57;
then A248: ( 2 in 17 \ (vars X1) & 3 in 17 \ (vars X1) & 4 in 17 \ (vars X1) & 5 in 17 \ (vars X1) & 6 in 17 \ (vars X1) & 7 in 17 \ (vars X1) ) by A235, XBOOLE_0:def 5;
then eval (X1,((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p))))) = eval (X1,(((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p))))) by Th53
.= eval (X1,((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p))))) by A248, Th53
.= eval (X1,(((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p))))) by A248, Th53
.= eval (X1,((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p))))) by A248, Th53
.= eval (X1,(p +* (7,(eval (V,p))))) by A248, Th53
.= eval (X1,p) by A248, Th53 ;
then A249: eval (Z1,((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p))))) = eval (Z,(((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p))))) by Th37, A234, NAT_1:44;
A250: len (((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) = 8 by AFINSQ_1:49;
A251: ( dom (((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) = 17 & Segm 8 c= Segm 17 ) by NAT_1:39, PARTFUN1:def 2;
then A252: ( dom ((((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) | 8) = 8 & rng ((((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) | 8) c= rng (((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) & rng (((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) c= the carrier of F_Real ) by RELAT_1:62, RELAT_1:70;
then reconsider p8 = (((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) | 8 as Function of 8,F_Real by FUNCT_2:2;
set ZR = <%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>;
A253: <%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%> = (((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ <%R1,P1,NN1,VV%> by AFINSQ_1:def 14
.= (((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ (((<%R1%> ^ <%P1%>) ^ <%NN1%>) ^ <%VV%>) by AFINSQ_1:def 14
.= ((((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ ((<%R1%> ^ <%P1%>) ^ <%NN1%>)) ^ <%VV%> by AFINSQ_1:27
.= (((((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ (<%R1%> ^ <%P1%>)) ^ <%NN1%>) ^ <%VV%> by AFINSQ_1:27
.= ((((((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ <%R1%>) ^ <%P1%>) ^ <%NN1%>) ^ <%VV%> by AFINSQ_1:27 ;
then A254: dom (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) = 8 by AFINSQ_1:49;
A255: ( dom (((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) = 17 & dom ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) = 17 & dom (((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) = 17 & dom ((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) = 17 & dom (((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) = 17 & dom ((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) = 17 & dom (p +* (7,(eval (V,p)))) = 17 & dom p = 17 ) by FUNCT_2:def 1;
A256: ( dom (x +* (0,z1)) = dom x & dom x = 17 & 17 = dom p ) by FUNCT_2:def 1, FUNCT_7:30;
for ii being object st ii in dom p holds
p . ii = (x +* (0,z1)) . ii

proof

let ii be object ; :: thesis: ( ii in dom p implies p . ii = (x +* (0,z1)) . ii )
assume A257: ii in dom p ; :: thesis: p . ii = (x +* (0,z1)) . ii
reconsider ii = ii as Nat by A257;

per cases ( ii = 0 or ii <> 0 ) ;

suppose A258: ii = 0 ; :: thesis: p . ii = (x +* (0,z1)) . ii

A259: 0 in Segm 8 by NAT_1:44;
p . 0 = (((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) . 0 by A259, A250, AFINSQ_1:def 3
.= z1 by AFINSQ_1:49 ;
hence p . ii = (x +* (0,z1)) . ii by A258, A256, A257, FUNCT_7:31; :: thesis: verum

end;

suppose A260: ii <> 0 ; :: thesis: p . ii = (x +* (0,z1)) . ii

per cases ( ii < Segm 8 or ii >= 8 ) ;

suppose ii < Segm 8 ; :: thesis: p . ii = (x +* (0,z1)) . ii

then A261: ( ii in 8 & 8 = Segm (7 + 1) ) by NAT_1:44;
A262: x . ii = (((((((<%0%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) . ii by A191, A261, AFINSQ_1:def 3;
A263: p . ii = (((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) . ii by A261, A250, AFINSQ_1:def 3;
not not ii = 0 & ... & not ii = 7 by A261, NAT_1:61;
then ( (((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) . ii = 0 & 0 = (((((((<%0%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) . ii ) by A260, AFINSQ_1:49;
hence p . ii = (x +* (0,z1)) . ii by A260, FUNCT_7:32, A262, A263; :: thesis: verum

end;

suppose ii >= 8 ; :: thesis: p . ii = (x +* (0,z1)) . ii

then reconsider jj = ii - 8 as Nat by NAT_1:21;
ii in Segm 17 by A257;
then jj + 8 < 8 + 9 by NAT_1:44;
then A264: jj in dom ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) by A192, NAT_1:44, XREAL_1:6;
A265: p . ii = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + jj)
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . jj by A264, A250, AFINSQ_1:def 3 ;
x . ii = ((((((((<%0%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + jj)
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . jj by A264, A191, AFINSQ_1:def 3 ;
hence p . ii = (x +* (0,z1)) . ii by A260, FUNCT_7:32, A265; :: thesis: verum

end;

end;

end;

end;

end;

then A266: x +* (0,z1) = p by A256;
A267: z1 in the carrier of F_Real by XREAL_0:def 1;
0 in Segm 8 by NAT_1:44;
then A268: p . 0 = (((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) . 0 by A250, AFINSQ_1:def 3
.= z1 by AFINSQ_1:49 ;
for ii being object st ii in dom (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) holds
(<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii

proof

let ii be object ; :: thesis: ( ii in dom (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) implies (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii )
assume A269: ii in dom (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) ; :: thesis: (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii
reconsider ii = ii as Nat by A269;
A270: ( p8 . ii = (((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . ii & ii in dom (((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) ) by A251, A269, A254, FUNCT_1:49;
ii in Segm (7 + 1) by A269, A253, AFINSQ_1:49;
then not not ii = 0 & ... & not ii = 7 by NAT_1:61;

per cases then ( ii = 0 or ii = 1 or ii = 2 or ii = 3 or ii = 4 or ii = 5 or ii = 6 or ii = 7 ) ;

suppose A271: ii = 0 ; :: thesis: (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii

( (((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . 0 = ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) . 0 & ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) . 0 = (((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) . 0 & (((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) . 0 = ((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) . 0 ) by FUNCT_7:32;
then ( (((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . 0 = (((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) . 0 & (((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) . 0 = ((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) . 0 & ((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) . 0 = (p +* (7,(eval (V,p)))) . 0 & (p +* (7,(eval (V,p)))) . 0 = p . 0 ) by FUNCT_7:32;
hence (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii by A253, AFINSQ_1:49, A268, A271, A270; :: thesis: verum

end;

suppose A272: ii = 1 ; :: thesis: (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii

not 0 in vars X1 by A1, A57;
then A273: 0 in 17 \ (vars X1) by A235, XBOOLE_0:def 5;
(((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . 1 = eval (X1,p) by A255, A251, A269, A254, A272, FUNCT_7:31
.= eval (X1,x) by A273, A267, Th53, A266 ;
hence (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii by A270, A272, A253, AFINSQ_1:49; :: thesis: verum

end;

suppose A274: ii = 2 ; :: thesis: (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii

not 0 in vars X2 by A1, A59;
then A275: 0 in 17 \ (vars X2) by A235, XBOOLE_0:def 5;
(((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . 2 = ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) . 2 by FUNCT_7:32
.= eval ((Four * X2),p) by A255, A251, A269, A254, A274, FUNCT_7:31
.= Four * (eval (X2,p)) by POLYNOM7:29
.= Four * (eval (X2,x)) by A275, A267, Th53, A266 ;
hence (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii by A270, A274, A253, AFINSQ_1:49; :: thesis: verum

end;

suppose A276: ii = 3 ; :: thesis: (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii

not 0 in vars X3 by A1, A62;
then A277: 0 in 17 \ (vars X3) by A235, XBOOLE_0:def 5;
(((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . 3 = ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) . 3 by FUNCT_7:32
.= (((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) . 3 by FUNCT_7:32
.= eval (((Four * Four) * X3),p) by A255, A251, A269, A254, A276, FUNCT_7:31
.= (Four * Four) * (eval (X3,p)) by POLYNOM7:29
.= (Four * Four) * (eval (X3,x)) by A277, A267, Th53, A266 ;
hence (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii by A270, A276, A253, AFINSQ_1:49; :: thesis: verum

end;

suppose A278: ii = 4 ; :: thesis: (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii

not 0 in vars R by A1, A66;
then A279: 0 in 17 \ (vars R) by A235, XBOOLE_0:def 5;
(((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . 4 = ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) . 4 by FUNCT_7:32
.= (((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) . 4 by FUNCT_7:32
.= ((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) . 4 by FUNCT_7:32
.= eval (R,p) by A255, A251, A269, A254, A278, FUNCT_7:31
.= eval (R,x) by A279, A267, Th53, A266 ;
hence (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii by A270, A278, A253, AFINSQ_1:49; :: thesis: verum

end;

suppose A280: ii = 5 ; :: thesis: (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii

not 0 in vars P by A1, A64;
then A281: 0 in 17 \ (vars P) by A235, XBOOLE_0:def 5;
(((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . 5 = ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) . 5 by FUNCT_7:32
.= (((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) . 5 by FUNCT_7:32
.= ((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) . 5 by FUNCT_7:32
.= (((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) . 5 by FUNCT_7:32
.= eval (P,p) by A255, A251, A269, A254, A280, FUNCT_7:31
.= eval (P,x) by A281, A267, Th53, A266 ;
hence (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii by A270, A280, A253, AFINSQ_1:49; :: thesis: verum

end;

suppose A282: ii = 6 ; :: thesis: (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii

not 0 in vars NN by A1, A103;
then A283: 0 in 17 \ (vars NN) by A235, XBOOLE_0:def 5;
(((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . 6 = ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) . 6 by FUNCT_7:32
.= (((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) . 6 by FUNCT_7:32
.= ((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) . 6 by FUNCT_7:32
.= (((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) . 6 by FUNCT_7:32
.= ((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) . 6 by FUNCT_7:32
.= eval (NN,p) by A255, A251, A269, A254, A282, FUNCT_7:31
.= eval (NN,x) by A283, A267, Th53, A266 ;
hence (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii by A270, A282, A253, AFINSQ_1:49; :: thesis: verum

end;

suppose A284: ii = 7 ; :: thesis: (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii

not 0 in vars V by A1, A102;
then A285: 0 in 17 \ (vars V) by A235, XBOOLE_0:def 5;
(((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) +* (1,(eval (X1,p)))) . 7 = ((((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) +* (2,(eval ((Four * X2),p)))) . 7 by FUNCT_7:32
.= (((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) +* (3,(eval (((Four * Four) * X3),p)))) . 7 by FUNCT_7:32
.= ((((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) +* (4,(eval (R,p)))) . 7 by FUNCT_7:32
.= (((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) +* (5,(eval (P,p)))) . 7 by FUNCT_7:32
.= ((p +* (7,(eval (V,p)))) +* (6,(eval (NN,p)))) . 7 by FUNCT_7:32
.= (p +* (7,(eval (V,p)))) . 7 by FUNCT_7:32
.= eval (V,p) by A255, A251, A269, A254, A284, FUNCT_7:31
.= eval (V,x) by A285, A267, Th53, A266 ;
hence (<%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%>) . ii = p8 . ii by A231, A270, A284, A253, AFINSQ_1:49; :: thesis: verum

end;

end;

end;

then p8 = <%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%> by A254, A252;
then A286: eval (K3,p8) = 0 by A233;
take p ; :: thesis: ( p /. 8 = k1 & p /. 9 is positive Nat & p /. 10 is positive Nat & p /. 11 is positive Nat & p /. 12 is positive Nat & p /. 13 is positive Nat & p /. 14 is Nat & p /. 15 is Nat & p /. 16 is Nat & p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
p /. 8 = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + 0) by A255, A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 0 by A194, A250, AFINSQ_1:def 3 ;
hence p /. 8 = k1 by AFINSQ_1:50; :: thesis: ( p /. 9 is positive Nat & p /. 10 is positive Nat & p /. 11 is positive Nat & p /. 12 is positive Nat & p /. 13 is positive Nat & p /. 14 is Nat & p /. 15 is Nat & p /. 16 is Nat & p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
A287: dom p = 17 by FUNCT_2:def 1;
p /. 9 = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + 1) by A287, A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 1 by A194, A250, AFINSQ_1:def 3 ;
hence p /. 9 is positive Nat by AFINSQ_1:50; :: thesis: ( p /. 10 is positive Nat & p /. 11 is positive Nat & p /. 12 is positive Nat & p /. 13 is positive Nat & p /. 14 is Nat & p /. 15 is Nat & p /. 16 is Nat & p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
p /. 10 = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + 2) by A287, A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 2 by A194, A250, AFINSQ_1:def 3 ;
hence p /. 10 is positive Nat by AFINSQ_1:50; :: thesis: ( p /. 11 is positive Nat & p /. 12 is positive Nat & p /. 13 is positive Nat & p /. 14 is Nat & p /. 15 is Nat & p /. 16 is Nat & p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
p /. 11 = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + 3) by A287, A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 3 by A194, A250, AFINSQ_1:def 3 ;
hence p /. 11 is positive Nat by AFINSQ_1:50; :: thesis: ( p /. 12 is positive Nat & p /. 13 is positive Nat & p /. 14 is Nat & p /. 15 is Nat & p /. 16 is Nat & p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
p /. 12 = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + 4) by A287, A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 4 by A194, A250, AFINSQ_1:def 3 ;
hence p /. 12 is positive Nat by AFINSQ_1:50; :: thesis: ( p /. 13 is positive Nat & p /. 14 is Nat & p /. 15 is Nat & p /. 16 is Nat & p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
p /. 13 = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + 5) by A287, A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 5 by A194, A250, AFINSQ_1:def 3 ;
hence p /. 13 is positive Nat by AFINSQ_1:50; :: thesis: ( p /. 14 is Nat & p /. 15 is Nat & p /. 16 is Nat & p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
p /. 14 = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + 6) by A287, A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 6 by A194, A250, AFINSQ_1:def 3 ;
hence p /. 14 is Nat by AFINSQ_1:50; :: thesis: ( p /. 15 is Nat & p /. 16 is Nat & p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
p /. 15 = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + 7) by A287, A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 7 by A194, A250, AFINSQ_1:def 3 ;
hence p /. 15 is Nat by AFINSQ_1:50; :: thesis: ( p /. 16 is Nat & p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
p /. 16 = ((((((((<%z1%> ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ <%0%>) ^ ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>)) . (8 + 8) by A287, A193, NAT_1:44, PARTFUN1:def 6
.= ((((((((<%k1%> ^ <%f1%>) ^ <%i1%>) ^ <%j1%>) ^ <%m1%>) ^ <%u1%>) ^ <%r1%>) ^ <%s1%>) ^ <%t1%>) . 8 by A194, A250, AFINSQ_1:def 3 ;
hence p /. 16 is Nat by AFINSQ_1:50; :: thesis: ( p /. 0 is Nat & eval (Z7,p) = 0. F_Real )
thus p /. 0 is Nat by A268, A287, A193, NAT_1:44, PARTFUN1:def 6; :: thesis: eval (Z7,p) = 0. F_Real
thus eval (Z7,p) = 0. F_Real by A236, A237, A239, A241, A244, A247, A249, A169, A286; :: thesis: verum

end;

given x being INT -valued Function of 17,F_Real such that A288: x /. 8 = k1 and
A289: ( x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) ; :: thesis: k1 + 1 is prime
reconsider f1 = x /. 9, i1 = x /. 10, j1 = x /. 11, m1 = x /. 12, u1 = x /. 13 as positive Nat by A289;
reconsider r1 = x /. 14, s1 = x /. 15, t1 = x /. 16, z1 = x /. 0 as Nat by A289;
A290: eval (W,x) = ((Hund * (x /. 9)) * (x /. 8)) * ((x /. 8) + (1. F_Real)) by A22;
reconsider W1 = eval (W,x) as Integer ;
A291: eval (U,x) = ((Hund * (u1 |^ 3)) * (W1 |^ 3)) + 1 by A24;
reconsider U1 = eval (U,x) as Integer ;
A292: eval (M,x) = (((Hund * (x /. 12)) * (eval (U,x))) * (eval (W,x))) + (1. F_Real) by A29;
reconsider M1 = eval (M,x) as Integer ;
eval (S,x) = ((((eval (M,x)) - (1. F_Real)) * (x /. 15)) + (x /. 8)) + (1. F_Real) by A31;
then A293: eval (S,x) = (((M1 - 1) * s1) + k1) + 1 by A288;
reconsider S1 = eval (S,x) as Integer ;
eval (T,x) = ((((((eval (M,x)) * (eval (U,x))) - (1. F_Real)) * (x /. 16)) + (eval (W,x))) - (x /. 8)) + (1. F_Real) by A33;
then A294: eval (T,x) = (((((M1 * U1) - 1) * t1) + W1) - k1) + 1 by A288;
reconsider T1 = eval (T,x) as Integer ;
A295: eval (Q,x) = (((Two * (eval (M,x))) * (eval (W,x))) - ((eval (W,x)) ^2)) - (1. F_Real) by A35;
reconsider Q1 = eval (Q,x) as Integer ;
A296: eval (L,x) = ((x /. 8) + (1. F_Real)) * (eval (Q,x)) by A37;
reconsider L1 = eval (L,x) as Integer ;
A297: eval (A,x) = (eval (M,x)) * ((eval (U,x)) + (1. F_Real)) by A39;
reconsider A1 = eval (A,x) as Integer ;
A298: eval (B,x) = (eval (W,x)) + (1. F_Real) by A41;
reconsider B1 = eval (B,x) as Integer ;
A299: eval (C,x) = ((x /. 14) + (eval (W,x))) + (1. F_Real) by A43;
reconsider C1 = eval (C,x) as Integer ;
A300: eval (D,x) = (((A1 ^2) - 1) * (C1 ^2)) + 1 by A45;
reconsider D1 = eval (D,x) as Integer ;
eval (E,x) = (((Two * (x /. 10)) * ((eval (C,x)) ^2)) * (eval (L,x))) * (eval (D,x)) by A47;
then A301: eval (E,x) = (((2 * i1) * (C1 ^2)) * L1) * D1 ;
reconsider E1 = eval (E,x) as Integer ;
A302: eval (F,x) = (((A1 ^2) - 1) * (E1 ^2)) + 1 by A50;
reconsider F1 = eval (F,x) as Integer ;
A303: eval (G,x) = (eval (A,x)) + ((eval (F,x)) * ((eval (F,x)) - (eval (A,x)))) by A52;
reconsider G1 = eval (G,x) as Integer ;
eval (H,x) = (eval (B,x)) + ((Two * ((x /. 11) - (1. F_Real))) * (eval (C,x))) by A54;
then A304: eval (H,x) = B1 + ((2 * (j1 - 1)) * C1) ;
reconsider H1 = eval (H,x) as Integer ;
A305: eval (I,x) = (((G1 ^2) - 1) * (H1 ^2)) + 1 by A56;
reconsider I1 = eval (I,x) as Integer ;
reconsider X11 = eval (X1,x), X21 = eval (X2,x) as odd Nat by A104, A171, A289, A288;
reconsider X31 = eval (X3,x), R1 = eval (R,x), NN1 = eval (NN,x) as Nat by A171, A289, A288, A104;
reconsider P1 = eval (P,x) as positive Nat by A171, A289, A288, A104;
reconsider V11 = eval (V1,x), V21 = eval (V2,x), V31 = eval (V3,x) as Integer ;
reconsider VV = ((V11 - V21) - V31) - 1 as Integer ;
A306: X11 = (((M1 ^2) - 1) * (S1 ^2)) + 1 by A58;
A307: eval (X2,x) = (((((eval (M,x)) * (eval (U,x))) ^2) - (1. F_Real)) * ((eval (T,x)) ^2)) + (1. F_Real) by A60;
A308: eval (X3,x) = ((eval (D,x)) * (eval (F,x))) * (eval (I,x)) by A63;
A309: eval (P,x) = (eval (F,x)) * (eval (L,x)) by A65;
A310: eval (R,x) = ((((eval (H,x)) - (eval (C,x))) * (eval (L,x))) + (((eval (F,x)) * ((x /. 9) + (1. F_Real))) * (eval (Q,x)))) + (((eval (F,x)) * ((x /. 8) + (1. F_Real))) * (((((((eval (W,x)) ^2) - (1. F_Real)) * (eval (S,x))) * (x /. 13)) - (((eval (W,x)) ^2) * ((x /. 13) ^2))) + (1. F_Real))) by A72;
reconsider V11 = eval (V1,x), V21 = eval (V2,x), V31 = eval (V3,x) as Integer ;
A311: eval (V1,x) = Eight * (((((x /. 9) * (x /. 13)) * (eval (S,x))) * (eval (T,x))) * ((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x))))) by A84;
A312: eval (V3,x) = ((Four * ((x /. 9) ^2)) - (1. F_Real)) * (((x /. 14) - ((((x /. 12) * (eval (S,x))) * (eval (T,x))) * (eval (U,x)))) ^2) by A93;
reconsider VV = ((V11 - V21) - V31) - 1 as Integer ;
A313: eval (V,x) = (eval (((V1 - V2) - V3),x)) - (eval ((1_ (17,F_Real)),x)) by POLYNOM2:24
.= (eval (((V1 - V2) - V3),x)) - (1. F_Real) by POLYNOM2:21
.= ((eval ((V1 - V2),x)) - (eval (V3,x))) - (1. F_Real) by POLYNOM2:24
.= (((eval (V1,x)) - (eval (V2,x))) - (eval (V3,x))) - (1. F_Real) by POLYNOM2:24 ;
A314: NN1 > (((sqrt X11) + (2 * (sqrt X21))) + (4 * (sqrt X31))) + R1 by A171, A289, A288, A104;
A315: 17 = Segm 17 ;
then A316: ( 0 in 17 & 1 in 17 & 2 in 17 & 3 in 17 & 4 in 17 & 5 in 17 & 6 in 17 & 7 in 17 ) by NAT_1:44;
set x7 = x +* (7,(eval (V,x)));
A317: eval (Z7,x) = eval (Z6,(x +* (7,(eval (V,x))))) by Th37, A315, NAT_1:44;
set x6 = (x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)));
not 7 in vars NN by A1, A103;
then 7 in 17 \ (vars NN) by A316, XBOOLE_0:def 5;
then eval (NN,(x +* (7,(eval (V,x))))) = eval (NN,x) by Th53;
then A318: eval (Z6,(x +* (7,(eval (V,x))))) = eval (Z5,((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x))))) by Th37, A315, NAT_1:44;
set x5 = ((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)));
( not 6 in vars P & not 7 in vars P ) by A1, A64;
then A319: ( 6 in 17 \ (vars P) & 7 in 17 \ (vars P) ) by A316, XBOOLE_0:def 5;
then eval (P,((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x))))) = eval (P,(x +* (7,(eval (V,x))))) by Th53
.= eval (P,x) by A319, Th53 ;
then A320: eval (Z5,((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x))))) = eval (Z4,(((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x))))) by Th37, A315, NAT_1:44;
set x4 = (((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)));
( not 5 in vars R & not 6 in vars R & not 7 in vars R ) by A1, A66;
then A321: ( 5 in 17 \ (vars R) & 6 in 17 \ (vars R) & 7 in 17 \ (vars R) ) by A316, XBOOLE_0:def 5;
then eval (R,(((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x))))) = eval (R,((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x))))) by Th53
.= eval (R,(x +* (7,(eval (V,x))))) by A321, Th53
.= eval (R,x) by A321, Th53 ;
then A322: eval (Z4,(((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x))))) = eval (Z3,((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x))))) by Th37, A315, NAT_1:44;
A323: vars ((Four * Four) * X3) c= 17 \ 8 by Th80, A62;
set x3 = ((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)));
( not 4 in vars ((Four * Four) * X3) & not 5 in vars ((Four * Four) * X3) & not 6 in vars ((Four * Four) * X3) & not 7 in vars ((Four * Four) * X3) ) by A1, A323;
then A324: ( 4 in 17 \ (vars ((Four * Four) * X3)) & 5 in 17 \ (vars ((Four * Four) * X3)) & 6 in 17 \ (vars ((Four * Four) * X3)) & 7 in 17 \ (vars ((Four * Four) * X3)) ) by A316, XBOOLE_0:def 5;
then eval (((Four * Four) * X3),((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x))))) = eval (((Four * Four) * X3),(((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x))))) by Th53
.= eval (((Four * Four) * X3),((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x))))) by A324, Th53
.= eval (((Four * Four) * X3),(x +* (7,(eval (V,x))))) by A324, Th53
.= eval (((Four * Four) * X3),x) by A324, Th53 ;
then A325: eval (Z3,((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x))))) = eval (Z2,(((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x))))) by Th37, A315, NAT_1:44;
A326: vars (Four * X2) c= 17 \ 8 by Th80, A59;
set x2 = (((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)));
( not 3 in vars (Four * X2) & not 4 in vars (Four * X2) & not 5 in vars (Four * X2) & not 6 in vars (Four * X2) & not 7 in vars (Four * X2) ) by A1, A326;
then A327: ( 3 in 17 \ (vars (Four * X2)) & 4 in 17 \ (vars (Four * X2)) & 5 in 17 \ (vars (Four * X2)) & 6 in 17 \ (vars (Four * X2)) & 7 in 17 \ (vars (Four * X2)) ) by A316, XBOOLE_0:def 5;
then eval ((Four * X2),(((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x))))) = eval ((Four * X2),((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x))))) by Th53
.= eval ((Four * X2),(((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x))))) by A327, Th53
.= eval ((Four * X2),((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x))))) by A327, Th53
.= eval ((Four * X2),(x +* (7,(eval (V,x))))) by A327, Th53
.= eval ((Four * X2),x) by A327, Th53 ;
then A328: eval (Z2,(((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x))))) = eval (Z1,((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x))))) by Th37, A315, NAT_1:44;
set x1 = ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)));
( not 2 in vars X1 & not 3 in vars X1 & not 4 in vars X1 & not 5 in vars X1 & not 6 in vars X1 & not 7 in vars X1 ) by A1, A57;
then A329: ( 2 in 17 \ (vars X1) & 3 in 17 \ (vars X1) & 4 in 17 \ (vars X1) & 5 in 17 \ (vars X1) & 6 in 17 \ (vars X1) & 7 in 17 \ (vars X1) ) by A316, XBOOLE_0:def 5;
then eval (X1,((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x))))) = eval (X1,(((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x))))) by Th53
.= eval (X1,((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x))))) by A329, Th53
.= eval (X1,(((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x))))) by A329, Th53
.= eval (X1,((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x))))) by A329, Th53
.= eval (X1,(x +* (7,(eval (V,x))))) by A329, Th53
.= eval (X1,x) by A329, Th53 ;
then A330: eval (Z1,((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x))))) = eval (Z,(((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x))))) by Th37, A315, NAT_1:44;
( dom (((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) = 17 & Segm 8 c= Segm 17 ) by NAT_1:39, PARTFUN1:def 2;
then ( dom ((((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) | 8) = 8 & rng ((((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) | 8) c= rng (((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) & rng (((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) c= the carrier of F_Real ) by RELAT_1:62, RELAT_1:70;
then reconsider x8 = (((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) | 8 as Function of 8,F_Real by FUNCT_2:2;
A331: for f being Function of 8,F_Real st f = <%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%> holds
0 = eval (K3,f)

proof

let ff be Function of 8,F_Real; :: thesis: ( ff = <%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%> implies 0 = eval (K3,ff) )
assume A332: ff = <%z1,X11,(4 * X21),(16 * X31)%> ^ <%R1,P1,NN1,VV%> ; :: thesis: 0 = eval (K3,ff)
A333: ff = (((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ <%R1,P1,NN1,VV%> by A332, AFINSQ_1:def 14
.= (((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ (((<%R1%> ^ <%P1%>) ^ <%NN1%>) ^ <%VV%>) by AFINSQ_1:def 14
.= ((((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ ((<%R1%> ^ <%P1%>) ^ <%NN1%>)) ^ <%VV%> by AFINSQ_1:27
.= (((((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ (<%R1%> ^ <%P1%>)) ^ <%NN1%>) ^ <%VV%> by AFINSQ_1:27
.= ((((((<%z1%> ^ <%X11%>) ^ <%(4 * X21)%>) ^ <%(16 * X31)%>) ^ <%R1%>) ^ <%P1%>) ^ <%NN1%>) ^ <%VV%> by AFINSQ_1:27 ;
then A334: dom ff = Segm 8 by AFINSQ_1:49;
A335: ( dom x = 17 & dom (((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) = 17 & dom ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) = 17 & dom (((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) = 17 & dom ((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) = 17 & dom (((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) = 17 & dom ((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) = 17 & dom (x +* (7,(eval (V,x)))) = 17 ) by FUNCT_2:def 1;
A336: 8 = dom x8 by FUNCT_2:def 1;
for ii being object st ii in dom ff holds
ff . ii = x8 . ii

proof

let ii be object ; :: thesis: ( ii in dom ff implies ff . ii = x8 . ii )
assume A337: ii in dom ff ; :: thesis: ff . ii = x8 . ii
reconsider ii = ii as Nat by A337, A333;
A338: ( x8 . ii = (((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . ii & ii in dom (((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) ) by A337, FUNCT_1:49, A336, RELAT_1:57;
ii in Segm (7 + 1) by A337;
then not not ii = 0 & ... & not ii = 7 by NAT_1:61;

per cases then ( ii = 0 or ii = 1 or ii = 2 or ii = 3 or ii = 4 or ii = 5 or ii = 6 or ii = 7 ) ;

suppose A339: ii = 0 ; :: thesis: ff . ii = x8 . ii

then A340: ff . ii = z1 by A333, AFINSQ_1:49;
( (((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . 0 = ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) . 0 & ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) . 0 = (((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) . 0 & (((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) . 0 = ((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) . 0 ) by FUNCT_7:32;
then ( (((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . 0 = (((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) . 0 & (((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) . 0 = ((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) . 0 & ((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) . 0 = (x +* (7,(eval (V,x)))) . 0 & (x +* (7,(eval (V,x)))) . 0 = x . 0 ) by FUNCT_7:32;
hence ff . ii = x8 . ii by A340, A339, A338, A335, PARTFUN1:def 6; :: thesis: verum

end;

suppose A341: ii = 1 ; :: thesis: ff . ii = x8 . ii

(((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . 1 = eval (X1,x) by A335, A338, A341, FUNCT_7:31;
hence ff . ii = x8 . ii by A338, A341, A333, AFINSQ_1:49; :: thesis: verum

end;

suppose A342: ii = 2 ; :: thesis: ff . ii = x8 . ii

(((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . 2 = ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) . 2 by FUNCT_7:32
.= eval ((Four * X2),x) by A335, A338, A342, FUNCT_7:31
.= Four * (eval (X2,x)) by POLYNOM7:29 ;
hence ff . ii = x8 . ii by A338, A342, A333, AFINSQ_1:49; :: thesis: verum

end;

suppose A343: ii = 3 ; :: thesis: ff . ii = x8 . ii

(((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . 3 = ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) . 3 by FUNCT_7:32
.= (((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) . 3 by FUNCT_7:32
.= eval (((Four * Four) * X3),x) by A335, A338, A343, FUNCT_7:31
.= (Four * Four) * (eval (X3,x)) by POLYNOM7:29 ;
hence ff . ii = x8 . ii by A338, A343, A333, AFINSQ_1:49; :: thesis: verum

end;

suppose A344: ii = 4 ; :: thesis: ff . ii = x8 . ii

(((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . 4 = ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) . 4 by FUNCT_7:32
.= (((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) . 4 by FUNCT_7:32
.= ((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) . 4 by FUNCT_7:32
.= eval (R,x) by A335, A338, A344, FUNCT_7:31 ;
hence ff . ii = x8 . ii by A338, A344, A333, AFINSQ_1:49; :: thesis: verum

end;

suppose A345: ii = 5 ; :: thesis: ff . ii = x8 . ii

(((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . 5 = ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) . 5 by FUNCT_7:32
.= (((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) . 5 by FUNCT_7:32
.= ((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) . 5 by FUNCT_7:32
.= (((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) . 5 by FUNCT_7:32
.= eval (P,x) by A335, A338, A345, FUNCT_7:31 ;
hence ff . ii = x8 . ii by A338, A345, A333, AFINSQ_1:49; :: thesis: verum

end;

suppose A346: ii = 6 ; :: thesis: ff . ii = x8 . ii

(((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . 6 = ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) . 6 by FUNCT_7:32
.= (((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) . 6 by FUNCT_7:32
.= ((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) . 6 by FUNCT_7:32
.= (((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) . 6 by FUNCT_7:32
.= ((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) . 6 by FUNCT_7:32
.= eval (NN,x) by A335, A338, A346, FUNCT_7:31 ;
hence ff . ii = x8 . ii by A338, A346, A333, AFINSQ_1:49; :: thesis: verum

end;

suppose A347: ii = 7 ; :: thesis: ff . ii = x8 . ii

(((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) +* (1,(eval (X1,x)))) . 7 = ((((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) +* (2,(eval ((Four * X2),x)))) . 7 by FUNCT_7:32
.= (((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) +* (3,(eval (((Four * Four) * X3),x)))) . 7 by FUNCT_7:32
.= ((((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) +* (4,(eval (R,x)))) . 7 by FUNCT_7:32
.= (((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) +* (5,(eval (P,x)))) . 7 by FUNCT_7:32
.= ((x +* (7,(eval (V,x)))) +* (6,(eval (NN,x)))) . 7 by FUNCT_7:32
.= (x +* (7,(eval (V,x)))) . 7 by FUNCT_7:32
.= eval (V,x) by A335, A338, A347, FUNCT_7:31 ;
hence ff . ii = x8 . ii by A313, A338, A347, A333, AFINSQ_1:49; :: thesis: verum

end;

end;

end;

then ff = x8 by A334;
hence 0 = eval (K3,ff) by A289, A169, A317, A318, A320, A322, A325, A328, A330; :: thesis: verum

end;

then A348: ( X11 is square & X21 is square & X31 is square & P1 divides R1 & VV >= 0 ) by A166, A314;
(((V11 - V21) - V31) - 1) + 1 > 0 by A331, A166, A314;
then (V11 - (V21 + V31)) + (V21 + V31) > 0 + (V21 + V31) by XREAL_1:8;
then (((4 * (f1 ^2)) - 1) * ((r1 - (((m1 * S1) * T1) * U1)) ^2)) + (((4 * (u1 ^2)) * (S1 ^2)) * (T1 ^2)) < ((((8 * f1) * u1) * S1) * T1) * (r1 - (((m1 * S1) * T1) * U1)) by A311, A87, A312;
hence k1 + 1 is prime by A171, HILB10_8:23, A297, A298, A299, A300, A301, A302, A303, A304, A305, A296, A290, A288, A291, A292, A293, A294, A295, A348, A308, A307, A306, A309, A310; :: thesis: verum

end;

A349: vars Z c= 8

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in vars Z or y in 8 )
assume y in vars Z ; :: thesis: y in 8
then consider b being bag of 17 such that
A350: ( b in Support Z & b . y <> 0 ) by Def5;
( y in dom b & dom b = 17 & 17 = Segm 17 ) by PARTFUN1:def 2, A350, FUNCT_1:def 2;
then reconsider y = y as Nat ;
y in Segm 8 by A168, A350, NAT_1:44;
hence y in 8 ; :: thesis: verum

end;

(vars Z) \ {1} c= 8 \ {1} by A349, XBOOLE_1:33;
then A351: ((vars Z) \ {1}) \/ (vars X1) c= (8 \ (Seg 1)) \/ (17 \ 8) by A57, XBOOLE_1:13, FINSEQ_1:2;
vars Z1 c= ((vars Z) \ {1}) \/ (vars X1) by Th47;
then A352: vars Z1 c= (8 \ (Seg 1)) \/ (17 \ 8) by A351;
A353: vars (Four * X2) c= 17 \ 8 by Th80, A59;
not 2 in 17 \ 8 by A1;
then (17 \ 8) \ {2} = 17 \ 8 by ZFMISC_1:57;
then ((8 \ (Seg 1)) \/ (17 \ 8)) \ {2} = ((8 \ (Seg 1)) \ {2}) \/ (17 \ 8) by XBOOLE_1:42
.= (8 \ ((Seg 1) \/ {(1 + 1)})) \/ (17 \ 8) by XBOOLE_1:41
.= (8 \ (Seg 2)) \/ (17 \ 8) by FINSEQ_1:9 ;
then (vars Z1) \ {2} c= (8 \ (Seg 2)) \/ (17 \ 8) by A352, XBOOLE_1:33;
then A354: ( ((vars Z1) \ {2}) \/ (vars (Four * X2)) c= ((8 \ (Seg 2)) \/ (17 \ 8)) \/ (17 \ 8) & ((8 \ (Seg 2)) \/ (17 \ 8)) \/ (17 \ 8) = (8 \ (Seg 2)) \/ ((17 \ 8) \/ (17 \ 8)) ) by A353, XBOOLE_1:4, XBOOLE_1:13;
vars Z2 c= ((vars Z1) \ {2}) \/ (vars (Four * X2)) by Th47;
then A355: vars Z2 c= (8 \ (Seg 2)) \/ (17 \ 8) by A354;
A356: vars ((Four * Four) * X3) c= 17 \ 8 by Th80, A62;
not 3 in 17 \ 8 by A1;
then (17 \ 8) \ {3} = 17 \ 8 by ZFMISC_1:57;
then ((8 \ (Seg 2)) \/ (17 \ 8)) \ {3} = ((8 \ (Seg 2)) \ {3}) \/ (17 \ 8) by XBOOLE_1:42
.= (8 \ ((Seg 2) \/ {(2 + 1)})) \/ (17 \ 8) by XBOOLE_1:41
.= (8 \ (Seg 3)) \/ (17 \ 8) by FINSEQ_1:9 ;
then (vars Z2) \ {3} c= (8 \ (Seg 3)) \/ (17 \ 8) by A355, XBOOLE_1:33;
then A357: ( ((vars Z2) \ {3}) \/ (vars ((Four * Four) * X3)) c= ((8 \ (Seg 3)) \/ (17 \ 8)) \/ (17 \ 8) & ((8 \ (Seg 3)) \/ (17 \ 8)) \/ (17 \ 8) = (8 \ (Seg 3)) \/ ((17 \ 8) \/ (17 \ 8)) ) by A356, XBOOLE_1:4, XBOOLE_1:13;
vars Z3 c= ((vars Z2) \ {3}) \/ (vars ((Four * Four) * X3)) by Th47;
then A358: vars Z3 c= (8 \ (Seg 3)) \/ (17 \ 8) by A357;
not 4 in 17 \ 8 by A1;
then (17 \ 8) \ {4} = 17 \ 8 by ZFMISC_1:57;
then ((8 \ (Seg 3)) \/ (17 \ 8)) \ {4} = ((8 \ (Seg 3)) \ {4}) \/ (17 \ 8) by XBOOLE_1:42
.= (8 \ ((Seg 3) \/ {(3 + 1)})) \/ (17 \ 8) by XBOOLE_1:41
.= (8 \ (Seg 4)) \/ (17 \ 8) by FINSEQ_1:9 ;
then (vars Z3) \ {4} c= (8 \ (Seg 4)) \/ (17 \ 8) by A358, XBOOLE_1:33;
then A359: ( ((vars Z3) \ {4}) \/ (vars R) c= ((8 \ (Seg 4)) \/ (17 \ 8)) \/ (17 \ 8) & ((8 \ (Seg 4)) \/ (17 \ 8)) \/ (17 \ 8) = (8 \ (Seg 4)) \/ ((17 \ 8) \/ (17 \ 8)) ) by A66, XBOOLE_1:4, XBOOLE_1:13;
vars Z4 c= ((vars Z3) \ {4}) \/ (vars R) by Th47;
then A360: vars Z4 c= (8 \ (Seg 4)) \/ (17 \ 8) by A359;
not 5 in 17 \ 8 by A1;
then (17 \ 8) \ {5} = 17 \ 8 by ZFMISC_1:57;
then ((8 \ (Seg 4)) \/ (17 \ 8)) \ {5} = ((8 \ (Seg 4)) \ {5}) \/ (17 \ 8) by XBOOLE_1:42
.= (8 \ ((Seg 4) \/ {(4 + 1)})) \/ (17 \ 8) by XBOOLE_1:41
.= (8 \ (Seg 5)) \/ (17 \ 8) by FINSEQ_1:9 ;
then (vars Z4) \ {5} c= (8 \ (Seg 5)) \/ (17 \ 8) by A360, XBOOLE_1:33;
then A361: ( ((vars Z4) \ {5}) \/ (vars P) c= ((8 \ (Seg 5)) \/ (17 \ 8)) \/ (17 \ 8) & ((8 \ (Seg 5)) \/ (17 \ 8)) \/ (17 \ 8) = (8 \ (Seg 5)) \/ ((17 \ 8) \/ (17 \ 8)) ) by A64, XBOOLE_1:4, XBOOLE_1:13;
vars Z5 c= ((vars Z4) \ {5}) \/ (vars P) by Th47;
then A362: vars Z5 c= (8 \ (Seg 5)) \/ (17 \ 8) by A361;
not 6 in 17 \ 8 by A1;
then (17 \ 8) \ {6} = 17 \ 8 by ZFMISC_1:57;
then ((8 \ (Seg 5)) \/ (17 \ 8)) \ {6} = ((8 \ (Seg 5)) \ {6}) \/ (17 \ 8) by XBOOLE_1:42
.= (8 \ ((Seg 5) \/ {(5 + 1)})) \/ (17 \ 8) by XBOOLE_1:41
.= (8 \ (Seg 6)) \/ (17 \ 8) by FINSEQ_1:9 ;
then (vars Z5) \ {6} c= (8 \ (Seg 6)) \/ (17 \ 8) by A362, XBOOLE_1:33;
then A363: ( ((vars Z5) \ {6}) \/ (vars NN) c= ((8 \ (Seg 6)) \/ (17 \ 8)) \/ (17 \ 8) & ((8 \ (Seg 6)) \/ (17 \ 8)) \/ (17 \ 8) = (8 \ (Seg 6)) \/ ((17 \ 8) \/ (17 \ 8)) ) by A103, XBOOLE_1:4, XBOOLE_1:13;
vars Z6 c= ((vars Z5) \ {6}) \/ (vars NN) by Th47;
then A364: vars Z6 c= (8 \ (Seg 6)) \/ (17 \ 8) by A363;
not 7 in 17 \ 8 by A1;
then (17 \ 8) \ {7} = 17 \ 8 by ZFMISC_1:57;
then ((8 \ (Seg 6)) \/ (17 \ 8)) \ {7} = ((8 \ (Seg 6)) \ {7}) \/ (17 \ 8) by XBOOLE_1:42
.= (8 \ ((Seg 6) \/ {(6 + 1)})) \/ (17 \ 8) by XBOOLE_1:41
.= (8 \ (Seg 7)) \/ (17 \ 8) by FINSEQ_1:9 ;
then (vars Z6) \ {7} c= (8 \ (Seg 7)) \/ (17 \ 8) by A364, XBOOLE_1:33;
then A365: ( ((vars Z6) \ {7}) \/ (vars V) c= ((8 \ (Seg 7)) \/ (17 \ 8)) \/ (17 \ 8) & ((8 \ (Seg 7)) \/ (17 \ 8)) \/ (17 \ 8) = (8 \ (Seg 7)) \/ ((17 \ 8) \/ (17 \ 8)) ) by A102, XBOOLE_1:4, XBOOLE_1:13;
A366: vars Z7 c= ((vars Z6) \ {7}) \/ (vars V) by Th47;
A367: not 0 in Seg 7 by FINSEQ_1:1;
7 + 1 = {0} \/ (Seg 7) by AFINSQ_1:4;
then 8 \ (Seg 7) = ({0} \ (Seg 7)) \/ ((Seg 7) \ (Seg 7)) by XBOOLE_1:42
.= {0} by A367, ZFMISC_1:59 ;
hence vars Z7 c= {0} \/ (17 \ 8) by A366, A365; :: thesis: for xk being Nat st xk > 0 holds
( xk + 1 is prime iff ex x being INT -valued Function of 17,F_Real st
( x /. 8 = xk & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) )
let xk be Nat; :: thesis: ( xk > 0 implies ( xk + 1 is prime iff ex x being INT -valued Function of 17,F_Real st
( x /. 8 = xk & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) ) )
thus ( xk > 0 implies ( xk + 1 is prime iff ex x being INT -valued Function of 17,F_Real st
( x /. 8 = xk & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z7,x) = 0. F_Real ) ) ) by A170; :: thesis: verum