consider p1 being INT -valued Polynomial of 17,F_Real such that
A1: vars p1 c= {0} \/ (17 \ 8) and
A2: 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 (p1,x) = 0. F_Real ) ) by Th82;
set N = 16;
set IN = idseq 16;
set E = 9;
set IE = idseq 9;
(idseq 16) | 9 = idseq 9 by FINSEQ_3:51;
then consider f being FinSequence such that
A3: idseq 16 = (idseq 9) ^ f by FINSEQ_1:80;
set R = f ^ (idseq 9);
set Z = id {0};
set RZ = (f ^ (idseq 9)) +* (id {0});
A4: ( rng (idseq 9) misses rng f & f is one-to-one ) by A3, FINSEQ_3:91;
A5: ( rng (idseq 16) = (rng (idseq 9)) \/ (rng f) & (rng (idseq 9)) \/ (rng f) = rng (f ^ (idseq 9)) ) by A3, FINSEQ_1:31;
A6: f ^ (idseq 9) is one-to-one by A4, FINSEQ_3:91;
A7: ( 16 = len (idseq 16) & len (idseq 16) = (len (idseq 9)) + (len f) & (len (idseq 9)) + (len f) = len (f ^ (idseq 9)) & len (idseq 9) = 9 ) by A3, FINSEQ_1:22;
then A8: dom (f ^ (idseq 9)) = Seg 16 by FINSEQ_1:def 3;
A9: ( rng (id {0}) = {0} & {0} = dom (id {0}) ) ;
not 0 in Seg 16 by FINSEQ_1:1;
then rng (id {0}) misses rng (f ^ (idseq 9)) by A5, ZFMISC_1:50;
then A10: (f ^ (idseq 9)) +* (id {0}) is one-to-one by A6, FUNCT_4:92;
A11: {0} \/ (Seg 16) = 16 + 1 by AFINSQ_1:4;
then A12: dom ((f ^ (idseq 9)) +* (id {0})) = 16 + 1 by A8, A9, FUNCT_4:def 1;
rng ((f ^ (idseq 9)) +* (id {0})) c= (rng (id {0})) \/ (rng (f ^ (idseq 9))) by FUNCT_4:17;
then reconsider RZ = (f ^ (idseq 9)) +* (id {0}) as Function of (16 + 1),(16 + 1) by A5, A11, A12, FUNCT_2:2;
card (16 + 1) = card (16 + 1) ;
then RZ is onto by A10, FINSEQ_4:63;
then reconsider RZ = RZ as Permutation of 17 by A10;
A13: not 0 in Seg 16 by FINSEQ_1:1;
A14: {0} c= {0} \/ (Seg 7) by XBOOLE_1:7;
A15: ( 16 + 1 = {0} \/ (Seg 16) & 7 + 1 = {0} \/ (Seg 7) ) by AFINSQ_1:4;
then A16: 17 \ 8 = ({0} \ ({0} \/ (Seg 7))) \/ ((Seg 16) \ ({0} \/ (Seg 7))) by XBOOLE_1:42
.= {} \/ ((Seg 16) \ ({0} \/ (Seg 7))) by A14
.= {} \/ (((Seg 16) \ {0}) \ (Seg 7)) by XBOOLE_1:41
.= (Seg 16) \ (Seg 7) by A13, ZFMISC_1:57 ;
A17: not 0 in Seg 7 by FINSEQ_1:1;
then ( {0} \ (Seg 7) = {0} & {0} misses Seg 7 ) by ZFMISC_1:59, ZFMISC_1:50;
then {0} \/ (17 \ 8) = 17 \ (Seg 7) by A15, A16, XBOOLE_1:42;
then A18: RZ .: (vars p1) c= RZ .: (17 \ (Seg 7)) by A1, RELAT_1:123;
A19: ( id {0} = 0 .--> 0 & 0 .--> 0 = {0} --> 0 ) by FUNCT_4:96, FUNCOP_1:def 9;
then A20: RZ .: (Seg 7) = (f ^ (idseq 9)) .: (Seg 7) by A17, ZFMISC_1:50, BOOLMARK:3;
A21: (f ^ (idseq 9)) .: (Seg 7) = ((f ^ (idseq 9)) | 7) .: (Seg 7) by RELAT_1:129
.= f .: (dom f) by A7, FINSEQ_1:def 3
.= rng f by RELAT_1:113 ;
RZ .: 17 = RZ .: (dom RZ) by A11, A8, A9, FUNCT_4:def 1
.= rng RZ by RELAT_1:113
.= 17 by FUNCT_2:def 3 ;
then A22: RZ .: (vars p1) c= 17 \ (rng f) by A18, FUNCT_1:64, A20, A21;
A23: (Segm 17) \ (rng f) c= Segm 10

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Segm 17) \ (rng f) or y in Segm 10 )
assume A24: y in (Segm 17) \ (rng f) ; :: thesis: y in Segm 10
assume A25: not y in Segm 10 ; :: thesis: contradiction
reconsider y = y as Nat by A24;
A26: y >= 9 + 1 by A25, NAT_1:44;
then A27: y > 9 by NAT_1:13;
then reconsider y1 = y - 9 as Nat by NAT_1:21;
y < 16 + 1 by A24, NAT_1:44;
then A28: y <= 16 by NAT_1:13;
then ( 9 - 9 < y - 9 & y - 9 <= 16 - 9 ) by A27, XREAL_1:6;
then ( 1 <= y1 & y1 <= len f ) by NAT_1:14, A7;
then A29: y1 in dom f by FINSEQ_3:25;
then A30: f . y1 = (idseq 16) . (y1 + 9) by A7, A3, FINSEQ_1:def 7;
1 <= y by A26, NAT_1:14;
then y in Seg 16 by A28;
then f . y1 = y by A30, FINSEQ_2:49;
then y in rng f by A29, FUNCT_1:def 3;
hence contradiction by A24, XBOOLE_0:def 5; :: thesis: verum

end;

A31: rng RZ = 17 by FUNCT_2:def 3;
A32: RZ . 0 = 0 by A19, FUNCT_4:113;
A33: 0 in Segm 17 by NAT_1:44;
then A34: (RZ ") . 0 = 0 by A32, A12, FUNCT_1:32;
A35: for i being Nat st 1 <= i & i <= 9 holds
( (RZ ") . i = i + 7 & RZ . (i + 7) = i )

proof

let i be Nat; :: thesis: ( 1 <= i & i <= 9 implies ( (RZ ") . i = i + 7 & RZ . (i + 7) = i ) )
assume A36: ( 1 <= i & i <= 9 ) ; :: thesis: ( (RZ ") . i = i + 7 & RZ . (i + 7) = i )
A37: ( i in dom (idseq 9) & i in Seg 9 ) by A36;
not i + 7 in dom (id {0}) ;
then A38: RZ . (i + 7) = (f ^ (idseq 9)) . (i + 7) by FUNCT_4:11
.= (idseq 9) . i by A37, A7, FINSEQ_1:def 7
.= i by A37, FINSEQ_2:49 ;
i + 7 <= 9 + 7 by A36, XREAL_1:6;
then i + 7 < 16 + 1 by NAT_1:13;
then i + 7 in Segm 17 by NAT_1:44;
hence ( (RZ ") . i = i + 7 & RZ . (i + 7) = i ) by A38, A12, FUNCT_1:32; :: thesis: verum

end;

set P2 = p1 permuted_by RZ;
A39: ( rng (p1 permuted_by RZ) = rng p1 & rng p1 c= INT ) by HILB10_2:26, RELAT_1:def 19;
then reconsider p2 = p1 permuted_by RZ as INT -valued Polynomial of (10 + 7),F_Real by RELAT_1:def 19;
vars p2 c= RZ .: (vars p1) by Th84;
then vars p2 c= Segm 10 by A23, A22;
then consider p3 being Polynomial of 10,F_Real such that
A40: ( vars p3 c= 10 & rng p3 c= rng p2 ) and
for b being bag of 10 + 7 holds
( ( b | 10 in Support p3 & ( for i being Nat st i >= 10 holds
b . i = 0 ) ) iff b in Support p2 ) and
for b being bag of 10 + 7 st b in Support p2 holds
p3 . (b | 10) = p2 . b and
A41: for x being Function of (10 + 7),F_Real
for y being Function of 10,F_Real st x | 10 = y holds
eval (p2,x) = eval (p3,y) by Th83;
A42: for xk being Nat st xk > 0 holds
( xk + 1 is prime iff ex x being INT -valued Function of 10,F_Real st
( x . 0 is Nat & x . 1 = xk & x . 2 is positive Nat & x . 3 is positive Nat & x . 4 is positive Nat & x . 5 is positive Nat & x . 6 is positive Nat & x . 7 is Nat & x . 8 is Nat & x . 9 is Nat & eval (p3,x) = 0. F_Real ) )

proof

let xk be Nat; :: thesis: ( xk > 0 implies ( xk + 1 is prime iff ex x being INT -valued Function of 10,F_Real st
( x . 0 is Nat & x . 1 = xk & x . 2 is positive Nat & x . 3 is positive Nat & x . 4 is positive Nat & x . 5 is positive Nat & x . 6 is positive Nat & x . 7 is Nat & x . 8 is Nat & x . 9 is Nat & eval (p3,x) = 0. F_Real ) ) )
assume A43: xk > 0 ; :: thesis: ( xk + 1 is prime iff ex x being INT -valued Function of 10,F_Real st
( x . 0 is Nat & x . 1 = xk & x . 2 is positive Nat & x . 3 is positive Nat & x . 4 is positive Nat & x . 5 is positive Nat & x . 6 is positive Nat & x . 7 is Nat & x . 8 is Nat & x . 9 is Nat & eval (p3,x) = 0. F_Real ) )
thus ( xk + 1 is prime implies ex x being INT -valued Function of 10,F_Real st
( x . 0 is Nat & x . 1 = xk & x . 2 is positive Nat & x . 3 is positive Nat & x . 4 is positive Nat & x . 5 is positive Nat & x . 6 is positive Nat & x . 7 is Nat & x . 8 is Nat & x . 9 is Nat & eval (p3,x) = 0. F_Real ) ) :: thesis: ( ex x being INT -valued Function of 10,F_Real st
( x . 0 is Nat & x . 1 = xk & x . 2 is positive Nat & x . 3 is positive Nat & x . 4 is positive Nat & x . 5 is positive Nat & x . 6 is positive Nat & x . 7 is Nat & x . 8 is Nat & x . 9 is Nat & eval (p3,x) = 0. F_Real ) implies xk + 1 is prime )

proof

assume xk + 1 is prime ; :: thesis: ex x being INT -valued Function of 10,F_Real st
( x . 0 is Nat & x . 1 = xk & x . 2 is positive Nat & x . 3 is positive Nat & x . 4 is positive Nat & x . 5 is positive Nat & x . 6 is positive Nat & x . 7 is Nat & x . 8 is Nat & x . 9 is Nat & eval (p3,x) = 0. F_Real )
then consider x being INT -valued Function of 17,F_Real such that
A44: ( 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 ) and
A45: eval (p1,x) = 0. F_Real by A2, A43;
reconsider xRZ = x * (RZ ") as INT -valued Function of (10 + 7),F_Real ;
A46: ( dom xRZ = 17 & Segm 10 c= Segm 17 ) by NAT_1:39, PARTFUN1:def 2;
then ( dom (xRZ | 10) = 10 & rng (xRZ | 10) c= rng xRZ & rng xRZ c= the carrier of F_Real ) by RELAT_1:62, RELAT_1:70;
then reconsider y = xRZ | 10 as INT -valued Function of 10,F_Real by FUNCT_2:2;
take y ; :: thesis: ( y . 0 is Nat & y . 1 = xk & y . 2 is positive Nat & y . 3 is positive Nat & y . 4 is positive Nat & y . 5 is positive Nat & y . 6 is positive Nat & y . 7 is Nat & y . 8 is Nat & y . 9 is Nat & eval (p3,y) = 0. F_Real )
0 in dom xRZ by A46, NAT_1:44;
then A47: (RZ ") . 0 in dom x by FUNCT_1:11;
0 in Segm 10 by NAT_1:44;
then y . 0 = xRZ . 0 by FUNCT_1:49
.= x . ((RZ ") . 0) by A46, NAT_1:44, FUNCT_1:12
.= x /. 0 by A47, A34, PARTFUN1:def 6 ;
hence y . 0 is Nat by A44; :: thesis: ( y . 1 = xk & y . 2 is positive Nat & y . 3 is positive Nat & y . 4 is positive Nat & y . 5 is positive Nat & y . 6 is positive Nat & y . 7 is Nat & y . 8 is Nat & y . 9 is Nat & eval (p3,y) = 0. F_Real )
A48: for i being Nat st 1 <= i & i <= 9 holds
y . i = x /. (i + 7)

proof

let i be Nat; :: thesis: ( 1 <= i & i <= 9 implies y . i = x /. (i + 7) )
assume A49: ( 1 <= i & i <= 9 ) ; :: thesis: y . i = x /. (i + 7)
A50: i < 17 by A49, XXREAL_0:2;
then i in dom xRZ by A46, NAT_1:44;
then A51: ( i + 7 = (RZ ") . i & (RZ ") . i in dom x ) by A49, A35, FUNCT_1:11;
i < 9 + 1 by A49, NAT_1:13;
then i in Segm 10 by NAT_1:44;
hence y . i = xRZ . i by FUNCT_1:49
.= x . ((RZ ") . i) by A50, A46, NAT_1:44, FUNCT_1:12
.= x /. (i + 7) by A51, PARTFUN1:def 6 ;
:: thesis: verum

end;

then y . 1 = x /. (1 + 7) ;
hence y . 1 = xk by A44; :: thesis: ( y . 2 is positive Nat & y . 3 is positive Nat & y . 4 is positive Nat & y . 5 is positive Nat & y . 6 is positive Nat & y . 7 is Nat & y . 8 is Nat & y . 9 is Nat & eval (p3,y) = 0. F_Real )
A52: ( y . 2 = x /. (2 + 7) & y . 3 = x /. (3 + 7) & y . 4 = x /. (4 + 7) & y . 5 = x /. (5 + 7) & y . 6 = x /. (6 + 7) & y . 7 = x /. (7 + 7) & y . 8 = x /. (8 + 7) & y . 9 = x /. (9 + 7) ) by A48;
0. F_Real = eval (p2,xRZ) by HILB10_2:25, A45
.= eval (p3,y) by A41 ;
hence ( y . 2 is positive Nat & y . 3 is positive Nat & y . 4 is positive Nat & y . 5 is positive Nat & y . 6 is positive Nat & y . 7 is Nat & y . 8 is Nat & y . 9 is Nat & eval (p3,y) = 0. F_Real ) by A52, A44; :: thesis: verum

end;

given x being INT -valued Function of 10,F_Real such that A53: ( x . 0 is Nat & x . 1 = xk & x . 2 is positive Nat & x . 3 is positive Nat & x . 4 is positive Nat & x . 5 is positive Nat & x . 6 is positive Nat & x . 7 is Nat & x . 8 is Nat & x . 9 is Nat & eval (p3,x) = 0. F_Real ) ; :: thesis: xk + 1 is prime
reconsider X7 = 7 --> 0 as XFinSequence of REAL ;
reconsider xx7 = (@ x) ^ X7 as 10 + 7 -element XFinSequence of REAL ;
reconsider XX7 = @ xx7 as INT -valued Function of 17,F_Real ;
A54: len (@ x) = 10 by CARD_1:def 7;
A55: ((@ x) ^ X7) | 10 = (@ x) | 10 by A54, AFINSQ_1:58
.= @ x ;
A56: dom XX7 = 17 by FUNCT_2:def 1;
(XX7 * RZ) * (RZ ") = XX7 * (RZ * (RZ ")) by RELAT_1:36
.= XX7 * (id 17) by A31, FUNCT_1:39
.= XX7 by A56, RELAT_1:51 ;
then A57: eval ((p1 permuted_by RZ),XX7) = eval (p1,(XX7 * RZ)) by HILB10_2:25;
ex y being INT -valued Function of 17,F_Real st
( y /. 8 = xk & y /. 9 is positive Nat & y /. 10 is positive Nat & y /. 11 is positive Nat & y /. 12 is positive Nat & y /. 13 is positive Nat & y /. 14 is Nat & y /. 15 is Nat & y /. 16 is Nat & y /. 0 is Nat & eval (p1,y) = 0. F_Real )

proof

take y = XX7 * RZ; :: thesis: ( y /. 8 = xk & y /. 9 is positive Nat & y /. 10 is positive Nat & y /. 11 is positive Nat & y /. 12 is positive Nat & y /. 13 is positive Nat & y /. 14 is Nat & y /. 15 is Nat & y /. 16 is Nat & y /. 0 is Nat & eval (p1,y) = 0. F_Real )
A58: dom y = 17 by FUNCT_2:def 1;
A59: for i being Nat st 1 <= i & i <= 9 holds
y /. (7 + i) = x . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= 9 implies y /. (7 + i) = x . i )
assume A60: ( 1 <= i & i <= 9 ) ; :: thesis: y /. (7 + i) = x . i
i + 7 <= 9 + 7 by A60, XREAL_1:6;
then i + 7 < 16 + 1 by NAT_1:13;
then A61: i + 7 in Segm 17 by NAT_1:44;
then A62: y /. (7 + i) = y . (7 + i) by A58, PARTFUN1:def 6
.= XX7 . (RZ . (7 + i)) by A61, A58, FUNCT_1:12 ;
A63: ( i = RZ . (7 + i) & RZ . (7 + i) in dom XX7 ) by A60, A35, A61, A58, FUNCT_1:11;
i < 9 + 1 by A60, NAT_1:13;
then i in Segm 10 by NAT_1:44;
hence y /. (7 + i) = x . i by A63, A62, A54, AFINSQ_1:def 3; :: thesis: verum

end;

A64: 0 in Segm 17 by NAT_1:44;
A65: y /. 0 = y . 0 by A33, A58, PARTFUN1:def 6
.= XX7 . (RZ . 0) by A64, A58, FUNCT_1:12 ;
A66: 0 in Segm 10 by NAT_1:44;
( x . 1 = y /. (1 + 7) & x . 2 = y /. (2 + 7) & x . 3 = y /. (3 + 7) & x . 4 = y /. (4 + 7) & x . 5 = y /. (5 + 7) & x . 6 = y /. (6 + 7) & x . 7 = y /. (7 + 7) & x . 8 = y /. (8 + 7) & x . 9 = y /. (9 + 7) ) by A59;
hence ( y /. 8 = xk & y /. 9 is positive Nat & y /. 10 is positive Nat & y /. 11 is positive Nat & y /. 12 is positive Nat & y /. 13 is positive Nat & y /. 14 is Nat & y /. 15 is Nat & y /. 16 is Nat & y /. 0 is Nat & eval (p1,y) = 0. F_Real ) by A53, A66, A65, A32, A54, AFINSQ_1:def 3, A55, A41, A57; :: thesis: verum

end;

hence xk + 1 is prime by A2, A43; :: thesis: verum

end;

rng p3 c= INT by A39, A40;
then reconsider p3 = p3 as INT -valued Polynomial of 10,F_Real by RELAT_1:def 19;
set EB = EmptyBag 10;
set O = 1_ (10,F_Real);
set P2 = (Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real));
set P3 = (Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real));
set P4 = (Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real));
set P5 = (Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real));
set P6 = (Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real));
reconsider Z2 = Subst (p3,2,((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real)))) as INT -valued Polynomial of 10,F_Real ;
reconsider Z3 = Subst (Z2,3,((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real)))) as INT -valued Polynomial of 10,F_Real ;
reconsider Z4 = Subst (Z3,4,((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real)))) as INT -valued Polynomial of 10,F_Real ;
reconsider Z5 = Subst (Z4,5,((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real)))) as INT -valued Polynomial of 10,F_Real ;
reconsider Z6 = Subst (Z5,6,((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real)))) as INT -valued Polynomial of 10,F_Real ;
take Z6 ; :: thesis: for k being positive Nat holds
( k + 1 is prime iff ex v being natural-valued Function of 10,F_Real st
( v . 1 = k & eval (Z6,v) = 0. F_Real ) )
let k be positive Nat; :: thesis: ( k + 1 is prime iff ex v being natural-valued Function of 10,F_Real st
( v . 1 = k & eval (Z6,v) = 0. F_Real ) )
A67: vars (1_ (10,F_Real)) = {} by Th38;
A68: 6 in Segm 10 by NAT_1:44;
A69: 5 in Segm 10 by NAT_1:44;
A70: (vars (Monom ((1. F_Real),((EmptyBag 10) +* (5,1))))) \/ (vars (1_ (10,F_Real))) c= {5} \/ {} by A67, Th48;
vars ((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))) c= (vars (Monom ((1. F_Real),((EmptyBag 10) +* (5,1))))) \/ (vars (1_ (10,F_Real))) by Th41;
then vars ((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))) c= {5} by A70;
then not 6 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))) by TARSKI:def 1;
then A71: 6 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real)))) by A68, XBOOLE_0:def 5;
A72: 4 in Segm 10 by NAT_1:44;
A73: (vars (Monom ((1. F_Real),((EmptyBag 10) +* (4,1))))) \/ (vars (1_ (10,F_Real))) c= {4} \/ {} by A67, Th48;
vars ((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))) c= (vars (Monom ((1. F_Real),((EmptyBag 10) +* (4,1))))) \/ (vars (1_ (10,F_Real))) by Th41;
then vars ((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))) c= {4} by A73;
then ( not 5 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))) & not 6 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))) ) by TARSKI:def 1;
then A74: ( 5 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real)))) & 6 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real)))) ) by A69, A68, XBOOLE_0:def 5;
A75: 3 in Segm 10 by NAT_1:44;
A76: (vars (Monom ((1. F_Real),((EmptyBag 10) +* (3,1))))) \/ (vars (1_ (10,F_Real))) c= {3} \/ {} by A67, Th48;
vars ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))) c= (vars (Monom ((1. F_Real),((EmptyBag 10) +* (3,1))))) \/ (vars (1_ (10,F_Real))) by Th41;
then vars ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))) c= {3} by A76;
then ( not 4 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))) & not 5 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))) & not 6 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))) ) by TARSKI:def 1;
then A77: ( 4 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real)))) & 5 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real)))) & 6 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real)))) ) by A72, A69, A68, XBOOLE_0:def 5;
A78: 2 in Segm 10 by NAT_1:44;
A79: (vars (Monom ((1. F_Real),((EmptyBag 10) +* (2,1))))) \/ (vars (1_ (10,F_Real))) c= {2} \/ {} by A67, Th48;
vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))) c= (vars (Monom ((1. F_Real),((EmptyBag 10) +* (2,1))))) \/ (vars (1_ (10,F_Real))) by Th41;
then vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))) c= {2} by A79;
then ( not 3 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))) & not 4 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))) & not 5 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))) & not 6 in vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))) ) by TARSKI:def 1;
then A80: ( 3 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real)))) & 4 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real)))) & 5 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real)))) & 6 in 10 \ (vars ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real)))) ) by A75, A72, A69, A68, XBOOLE_0:def 5;
thus ( k + 1 is prime implies ex v being natural-valued Function of 10,F_Real st
( v . 1 = k & eval (Z6,v) = 0. F_Real ) ) :: thesis: ( ex v being natural-valued Function of 10,F_Real st
( v . 1 = k & eval (Z6,v) = 0. F_Real ) implies k + 1 is prime )

proof

assume k + 1 is prime ; :: thesis: ex v being natural-valued Function of 10,F_Real st
( v . 1 = k & eval (Z6,v) = 0. F_Real )
then consider x being INT -valued Function of 10,F_Real such that
A81: ( x . 0 is Nat & x . 1 = k & x . 2 is positive Nat & x . 3 is positive Nat & x . 4 is positive Nat & x . 5 is positive Nat & x . 6 is positive Nat & x . 7 is Nat & x . 8 is Nat & x . 9 is Nat ) and
A82: eval (p3,x) = 0. F_Real by A42;
reconsider x0 = x . 0, x1 = x . 1, x7 = x . 7, x8 = x . 8, x9 = x . 9 as Element of NAT by A81, ORDINAL1:def 12;
reconsider x2 = (x . 2) - 1, x3 = (x . 3) - 1, x4 = (x . 4) - 1, x5 = (x . 5) - 1, x6 = (x . 6) - 1 as Element of NAT by A81, NAT_1:20;
set v = (((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>;
set V = ((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%>;
reconsider VV = @ (((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%>) as natural-valued Function of 10,F_Real ;
take VV ; :: thesis: ( VV . 1 = k & eval (Z6,VV) = 0. F_Real )
A83: len ((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) = 9 by AFINSQ_1:50;
A84: len (((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%>) = Segm 10 by CARD_1:def 7;
A85: ( 2 in Segm 9 & 3 in Segm 9 & 4 in Segm 9 & 5 in Segm 9 & 6 in Segm 9 ) by NAT_1:44;
set VV6 = VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)));
A86: eval (Z6,VV) = eval (Z5,(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) by A68, Th37;
A87: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 6)) + (eval ((1_ (10,F_Real)),VV)) by A68, Th27
.= (VV /. 6) + 1 by POLYNOM2:21
.= (VV . 6) + 1 by A84, NAT_1:44, PARTFUN1:def 6
.= (((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 6) + 1 by A85, A83, AFINSQ_1:def 3
.= x6 + 1 by AFINSQ_1:50 ;
set VV5 = (VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)));
eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV) by Th53, A71;
then A88: eval (Z5,(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) = eval (Z4,((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) by A69, Th37;
A89: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 5)) + (eval ((1_ (10,F_Real)),VV)) by A69, Th27
.= (VV /. 5) + 1 by POLYNOM2:21
.= (VV . 5) + 1 by A84, NAT_1:44, PARTFUN1:def 6
.= (((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 5) + 1 by A85, A83, AFINSQ_1:def 3
.= x5 + 1 by AFINSQ_1:50 ;
set VV4 = ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)));
eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A74
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV) by Th53, A74 ;
then A90: eval (Z4,((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) = eval (Z3,(((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV))))) by A72, Th37;
A91: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 4)) + (eval ((1_ (10,F_Real)),VV)) by A72, Th27
.= (VV /. 4) + 1 by POLYNOM2:21
.= (VV . 4) + 1 by A84, NAT_1:44, PARTFUN1:def 6
.= (((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 4) + 1 by A85, A83, AFINSQ_1:def 3
.= x4 + 1 by AFINSQ_1:50 ;
set VV3 = (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)));
eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),(((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV))))) = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A77
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A77
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV) by Th53, A77 ;
then A92: eval (Z3,(((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV))))) = eval (Z2,((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV))))) by A75, Th37;
A93: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 3)) + (eval ((1_ (10,F_Real)),VV)) by A75, Th27
.= (VV /. 3) + 1 by POLYNOM2:21
.= (VV . 3) + 1 by A84, NAT_1:44, PARTFUN1:def 6
.= (((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 3) + 1 by A85, A83, AFINSQ_1:def 3
.= x3 + 1 by AFINSQ_1:50 ;
set VV2 = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)));
A94: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV))))) = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),(((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A80
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A80
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A80
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV) by Th53, A80 ;
A95: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 2)) + (eval ((1_ (10,F_Real)),VV)) by A78, Th27
.= (VV /. 2) + 1 by POLYNOM2:21
.= (VV . 2) + 1 by A84, NAT_1:44, PARTFUN1:def 6
.= (((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 2) + 1 by A85, A83, AFINSQ_1:def 3
.= x2 + 1 by AFINSQ_1:50 ;
A96: Segm 10 = dom (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) by FUNCT_2:def 1;
1 in Segm 9 by NAT_1:44;
then VV . 1 = ((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 1 by A83, AFINSQ_1:def 3
.= x1 by AFINSQ_1:50 ;
hence VV . 1 = k by A81; :: thesis: eval (Z6,VV) = 0. F_Real
for y being object st y in dom (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) holds
x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y

proof

let y be object ; :: thesis: ( y in dom (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) implies x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y )
assume A97: y in dom (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) ; :: thesis: x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y
then reconsider y = y as Nat by A84;
y < 9 + 1 by A97, A84, NAT_1:44;
then y <= 9 by NAT_1:13;
then not not y = 0 & ... & not y = 9 ;

per cases then ( y = 0 or y = 1 or y = 7 or y = 8 or y = 9 or not not y = 2 & ... & not y = 6 ) ;

suppose A98: ( y = 0 or y = 1 or y = 7 or y = 8 or y = 9 ) ; :: thesis: x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y

then A99: (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . y by FUNCT_7:32
.= (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) . y by A98, FUNCT_7:32
.= ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) . y by A98, FUNCT_7:32
.= (VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) . y by A98, FUNCT_7:32
.= VV . y by A98, FUNCT_7:32 ;
VV . y = x . y

proof

per cases ( y = 9 or y <> 9 ) ;

suppose y = 9 ; :: thesis: VV . y = x . y

hence VV . y = x . y by A83, AFINSQ_1:36; :: thesis: verum

end;

suppose A100: y <> 9 ; :: thesis: VV . y = x . y

then y in Segm 9 by A98, NAT_1:44;
hence VV . y = ((((((((<%x0%> ^ <%x1%>) ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . y by A83, AFINSQ_1:def 3
.= x . y by A98, A100, AFINSQ_1:50 ;
:: thesis: verum

end;

end;

end;

hence x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y by A99; :: thesis: verum

end;

suppose A101: not not y = 2 & ... & not y = 6 ; :: thesis: x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y

A102: ( dom (VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) = 10 & dom ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) = 10 ) by FUNCT_2:def 1;
A103: ( dom (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) = 10 & dom ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) = 10 ) by FUNCT_2:def 1;

per cases ( y = 6 or y = 5 or y = 4 or y = 3 or y = 2 ) by A101;

suppose A104: y = 6 ; :: thesis: x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y

then (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . y by FUNCT_7:32
.= (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) . y by A104, FUNCT_7:32
.= ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) . y by A104, FUNCT_7:32
.= (VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) . y by A104, FUNCT_7:32
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV) by A104, A84, NAT_1:44, FUNCT_7:31 ;
hence x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y by A87, A104; :: thesis: verum

end;

suppose A105: y = 5 ; :: thesis: x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y

then (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . y by FUNCT_7:32
.= (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) . y by A105, FUNCT_7:32
.= ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) . y by A105, FUNCT_7:32
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV) by A102, A105, A69, FUNCT_7:31 ;
hence x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y by A89, A105; :: thesis: verum

end;

suppose A106: y = 4 ; :: thesis: x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y

then (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . y by FUNCT_7:32
.= (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) . y by A106, FUNCT_7:32
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV) by A102, A106, A72, FUNCT_7:31 ;
hence x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y by A91, A106; :: thesis: verum

end;

suppose A107: y = 3 ; :: thesis: x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y

then (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . y by FUNCT_7:32
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV) by A103, A107, A75, FUNCT_7:31 ;
hence x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y by A93, A107; :: thesis: verum

end;

suppose y = 2 ; :: thesis: x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y

hence x . y = (((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)))) . y by A95, A103, A78, FUNCT_7:31; :: thesis: verum

end;

end;

end;

end;

end;

then x = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV))) by A96;
hence eval (Z6,VV) = 0. F_Real by A82, A88, A86, A90, A92, A94, A78, Th37; :: thesis: verum

end;

given VV being natural-valued Function of 10,F_Real such that A108: ( VV . 1 = k & eval (Z6,VV) = 0. F_Real ) ; :: thesis: k + 1 is prime
A109: dom VV = Segm 10 by FUNCT_2:def 1;
set VV6 = VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)));
A110: eval (Z6,VV) = eval (Z5,(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) by A68, Th37;
A111: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 6)) + (eval ((1_ (10,F_Real)),VV)) by A68, Th27
.= (VV /. 6) + 1 by POLYNOM2:21
.= (VV . 6) + 1 by A109, NAT_1:44, PARTFUN1:def 6 ;
then reconsider e6 = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV) as Element of INT by INT_1:def 1;
set VV5 = (VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)));
eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV) by Th53, A71;
then A112: eval (Z5,(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) = eval (Z4,((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) by A69, Th37;
A113: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 5)) + (eval ((1_ (10,F_Real)),VV)) by A69, Th27
.= (VV /. 5) + 1 by POLYNOM2:21
.= (VV . 5) + 1 by A109, NAT_1:44, PARTFUN1:def 6 ;
then reconsider e5 = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV) as Element of INT by INT_1:def 1;
set VV4 = ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)));
eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A74
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV) by Th53, A74 ;
then A114: eval (Z4,((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) = eval (Z3,(((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV))))) by A72, Th37;
A115: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 4)) + (eval ((1_ (10,F_Real)),VV)) by A72, Th27
.= (VV /. 4) + 1 by POLYNOM2:21
.= (VV . 4) + 1 by A109, NAT_1:44, PARTFUN1:def 6 ;
then reconsider e4 = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV) as Element of INT by INT_1:def 1;
set VV3 = (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)));
eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),(((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV))))) = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A77
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A77
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV) by Th53, A77 ;
then A116: eval (Z3,(((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV))))) = eval (Z2,((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV))))) by A75, Th37;
A117: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 3)) + (eval ((1_ (10,F_Real)),VV)) by A75, Th27
.= (VV /. 3) + 1 by POLYNOM2:21
.= (VV . 3) + 1 by A109, NAT_1:44, PARTFUN1:def 6 ;
then reconsider e3 = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV) as Element of INT by INT_1:def 1;
set VV2 = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV)));
eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV))))) = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),(((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A80
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A80
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),(VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV))))) by Th53, A80
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV) by Th53, A80 ;
then A118: eval (Z2,((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV))))) = eval (p3,(((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV))))) by A78, Th37;
A119: eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV) = (eval ((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))),VV)) + (eval ((1_ (10,F_Real)),VV)) by POLYNOM2:23
.= ((1. F_Real) * (VV /. 2)) + (eval ((1_ (10,F_Real)),VV)) by A78, Th27
.= (VV /. 2) + 1 by POLYNOM2:21
.= (VV . 2) + 1 by A109, NAT_1:44, PARTFUN1:def 6 ;
then reconsider e2 = eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV) as Element of INT by INT_1:def 1;
((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV))) = ((((VV +* (6,e6)) +* (5,e5)) +* (4,e4)) +* (3,e3)) +* (2,e2) ;
then reconsider VV2 = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) +* (2,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (2,1)))) + (1_ (10,F_Real))),VV))) as INT -valued Function of 10,F_Real ;
A120: for y being Nat st ( y = 0 or y = 1 or y = 7 or y = 8 or y = 9 ) holds
VV2 . y = VV . y

proof

let y be Nat; :: thesis: ( ( y = 0 or y = 1 or y = 7 or y = 8 or y = 9 ) implies VV2 . y = VV . y )
assume A121: ( y = 0 or y = 1 or y = 7 or y = 8 or y = 9 ) ; :: thesis: VV2 . y = VV . y
hence VV2 . y = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . y by FUNCT_7:32
.= (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) . y by A121, FUNCT_7:32
.= ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) . y by A121, FUNCT_7:32
.= (VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) . y by A121, FUNCT_7:32
.= VV . y by A121, FUNCT_7:32 ;
:: thesis: verum

end;

( VV . 0 is Nat & VV . 7 is Nat & VV . 8 is Nat & VV . 9 is Nat ) ;
then A122: ( VV2 . 0 is Nat & VV2 . 7 is Nat & VV2 . 8 is Nat & VV2 . 9 is Nat ) by A120;
A123: VV2 . 1 = k by A120, A108;
A124: VV2 . 6 = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . 6 by FUNCT_7:32
.= (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) . 6 by FUNCT_7:32
.= ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) . 6 by FUNCT_7:32
.= (VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) . 6 by FUNCT_7:32
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV) by A109, NAT_1:44, FUNCT_7:31 ;
A125: ( dom (VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) = 10 & dom ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) = 10 ) by FUNCT_2:def 1;
A126: ( dom (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) = 10 & dom ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) = 10 ) by FUNCT_2:def 1;
A127: VV2 . 5 = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . 5 by FUNCT_7:32
.= (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) . 5 by FUNCT_7:32
.= ((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) . 5 by FUNCT_7:32
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV) by A125, A69, FUNCT_7:31 ;
A128: VV2 . 4 = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . 4 by FUNCT_7:32
.= (((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) . 4 by FUNCT_7:32
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV) by A125, A72, FUNCT_7:31 ;
A129: VV2 . 3 = ((((VV +* (6,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (6,1)))) + (1_ (10,F_Real))),VV)))) +* (5,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (5,1)))) + (1_ (10,F_Real))),VV)))) +* (4,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (4,1)))) + (1_ (10,F_Real))),VV)))) +* (3,(eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV)))) . 3 by FUNCT_7:32
.= eval (((Monom ((1. F_Real),((EmptyBag 10) +* (3,1)))) + (1_ (10,F_Real))),VV) by A126, A75, FUNCT_7:31 ;
VV2 . 2 = (VV . 2) + 1 by A119, A126, A78, FUNCT_7:31;
hence k + 1 is prime by A42, A122, A123, A124, A127, A113, A128, A129, A117, A108, A115, A118, A116, A114, A112, A110, A111; :: thesis: verum