let M be Jpolynom of 4, F_Complex ; :: thesis:
set p = Jsqrt M;
set R = F_Real ;
consider q being Polynomial of (4 + 2),F_Real such that
A1: rng q c= (rng (Jsqrt M)) \/ {(0. F_Real)} and
A2: for b being bag of 4 + 2 holds
( b in Support q iff ( b | 4 in Support (Jsqrt M) & ( for i being Nat st i >= 4 holds
b . i = 0 ) ) ) and
A3: for b being bag of 4 + 2 st b in Support q holds
q . b = (Jsqrt M) . (b | 4) and
A4: for x being Function of 4,F_Real
for y being Function of (4 + 2),F_Real st y | 4 = x holds
eval ((Jsqrt M),x) = eval (q,y) by Th75;
rng q c= INT by A1, INT_1:def 2;
then reconsider q = q as INT -valued Polynomial of 6,F_Real by RELAT_1:def 19;
set Yb = (EmptyBag 6) +* (0,1);
set Y = Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)));
set Zb = (EmptyBag 6) +* (4,1);
set Z = Monom ((1. F_Real),((EmptyBag 6) +* (4,1)));
set YZ = (Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))));
set Sup = SgmX ((BagOrder 6),(Support q));
BagOrder 6 linearly_orders Support q by POLYNOM2:18;
then A5: rng (SgmX ((BagOrder 6),(Support q))) = Support q by PRE_POLY:def 2;
consider S being FinSequence of (Polynom-Ring (6,F_Real)) such that
A6: ( Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))) = Sum S & len (SgmX ((BagOrder 6),(Support q))) = len S ) and
A7: for i being Nat st i in dom S holds
S . i = (q . ((SgmX ((BagOrder 6),(Support q))) /. i)) * (Subst (((SgmX ((BagOrder 6),(Support q))) /. i),0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) by Def4;
A8: dom S = dom (SgmX ((BagOrder 6),(Support q))) by A6, FINSEQ_3:29;
4 -' 1 = 4 - 1 by XREAL_1:233;
then A9: 2 |^ (4 -' 1) = 2 |^ (2 + 1)
.= 2 * (2 |^ (1 + 1)) by NEWTON:6
.= 2 * (2 * (2 |^ 1)) by NEWTON:6
.= 8 ;
set E6 = EmptyBag 6;
set MAX = (EmptyBag 4) +* (0,8);
set MAX8 = (EmptyBag 6) +* (0,8);
A10: M . ((EmptyBag 4) +* (0,8)) = 1. F_Complex by Def10, A9;
A11: ( (EmptyBag 4) +* (0,8) in Bags 4 & Bags 4 = dom (Jsqrt M) ) by FUNCT_2:def 1, PRE_POLY:def 12;
(2 (#) ((EmptyBag 4) +* (0,8))) +* (0,(((EmptyBag 4) +* (0,8)) . 0)) = (EmptyBag 4) +* (0,8)

A12: ( dom (2 (#) ((EmptyBag 4) +* (0,8))) = 4 & 4 = dom ((2 (#) ((EmptyBag 4) +* (0,8))) +* (0,(((EmptyBag 4) +* (0,8)) . 0))) ) by PARTFUN1:def 2;
for x being object st x in 4 holds
((EmptyBag 4) +* (0,8)) . x = ((2 (#) ((EmptyBag 4) +* (0,8))) +* (0,(((EmptyBag 4) +* (0,8)) . 0))) . x

let x be object ; :: thesis:
assume A13: x in 4 ; :: thesis:

per cases ;

suppose x = 0 ; :: thesis:

hence ((EmptyBag 4) +* (0,8)) . x = ((2 (#) ((EmptyBag 4) +* (0,8))) +* (0,(((EmptyBag 4) +* (0,8)) . 0))) . x by A12, A13, FUNCT_7:31; :: thesis:

end;

suppose A14: x <> 0 ; :: thesis:

then A15: ((EmptyBag 4) +* (0,8)) . x = (EmptyBag 4) . x by FUNCT_7:32
.= 0 ;
2 * (((EmptyBag 4) +* (0,8)) . x) = (2 (#) ((EmptyBag 4) +* (0,8))) . x by A12, A13, VALUED_1:def 5
.= ((2 (#) ((EmptyBag 4) +* (0,8))) +* (0,(((EmptyBag 4) +* (0,8)) . 0))) . x by A14, FUNCT_7:32 ;
hence ((EmptyBag 4) +* (0,8)) . x = ((2 (#) ((EmptyBag 4) +* (0,8))) +* (0,(((EmptyBag 4) +* (0,8)) . 0))) . x by A15; :: thesis:

end;

hence (2 (#) ((EmptyBag 4) +* (0,8))) +* (0,(((EmptyBag 4) +* (0,8)) . 0)) = (EmptyBag 4) +* (0,8) by A12, PARTFUN1:def 2; :: thesis:

end;

then (JsqrtSeries M) . ((EmptyBag 4) +* (0,8)) = M . ((EmptyBag 4) +* (0,8)) by Def12;
then A16: (Jsqrt M) . ((EmptyBag 4) +* (0,8)) = 1. F_Complex by Def13, A10
.= 1. F_Real by COMPLEX1:def 4, COMPLFLD:def 1 ;
then (Jsqrt M) . ((EmptyBag 4) +* (0,8)) <> 0. F_Real ;
then A17: (EmptyBag 4) +* (0,8) in Support (Jsqrt M) by A11, POLYNOM1:def 3;
A18: ( dom (EmptyBag 6) = 6 & dom (EmptyBag 4) = 4 ) by PARTFUN1:def 2;
A19: ( 4 in Segm 6 & 0 in Segm 6 & 5 in Segm 6 ) by NAT_1:44;
A20: ((EmptyBag 6) +* (0,8)) . 0 = 8 by A18, A19, FUNCT_7:31;
A21: Segm 4 c= Segm 6 by NAT_1:39;
A22: dom (((EmptyBag 6) +* (0,8)) | 4) = 4 by PARTFUN1:def 2, A21;
for x being object st x in 4 holds
(((EmptyBag 6) +* (0,8)) | 4) . x = ((EmptyBag 4) +* (0,8)) . x

proof

let x be object ; :: thesis:
assume A23: x in 4 ; :: thesis:
A24: (((EmptyBag 6) +* (0,8)) | 4) . x = ((EmptyBag 6) +* (0,8)) . x by A23, FUNCT_1:49;

per cases ;

suppose x = 0 ; :: thesis:

hence (((EmptyBag 6) +* (0,8)) | 4) . x = ((EmptyBag 4) +* (0,8)) . x by A18, A20, A24, A23, FUNCT_7:31; :: thesis:

end;

suppose A25: x <> 0 ; :: thesis:

then ( (((EmptyBag 6) +* (0,8)) | 4) . x = (EmptyBag 6) . x & (EmptyBag 6) . x = (EmptyBag 4) . x ) by A24, FUNCT_7:32;
hence (((EmptyBag 6) +* (0,8)) | 4) . x = ((EmptyBag 4) +* (0,8)) . x by A25, FUNCT_7:32; :: thesis:

end;

then A26: ((EmptyBag 6) +* (0,8)) | 4 = (EmptyBag 4) +* (0,8) by PARTFUN1:def 2, A22;
A27: for i being Nat st i >= 4 holds
((EmptyBag 6) +* (0,8)) . i = 0

proof

let i be Nat; :: thesis:
assume A28: i >= 4 ; :: thesis:
((EmptyBag 6) +* (0,8)) . i = (EmptyBag 6) . i by A28, FUNCT_7:32;
hence ((EmptyBag 6) +* (0,8)) . i = 0 ; :: thesis:

end;

(EmptyBag 6) +* (0,8) in Support q by A2, A26, A17, A27;
then consider I being object such that
A29: ( I in dom (SgmX ((BagOrder 6),(Support q))) & (SgmX ((BagOrder 6),(Support q))) . I = (EmptyBag 6) +* (0,8) ) by A5, FUNCT_1:def 3;
A30: q . ((EmptyBag 6) +* (0,8)) = 1. F_Real by A16, A17, A26, A27, A3, A2;
reconsider I = I as Nat by A29;
A31: ( (SgmX ((BagOrder 6),(Support q))) /. I = (SgmX ((BagOrder 6),(Support q))) . I & S /. I = S . I ) by A8, A29, PARTFUN1:def 6;
defpred S₁[ Nat] means (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ $1) . ((EmptyBag 6) +* (4,$1)) = 1. F_Real;
A32: ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ 0 = 1_ (6,F_Real) by Th28;
(EmptyBag 6) . 4 = 0 ;
then (EmptyBag 6) +* (4,0) = EmptyBag 6 by FUNCT_7:35;
then A33: S₁[ 0 ] by A32, POLYNOM1:25;
A34: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

end;

A43: for i being Nat holds S₁[i] from NAT_1:sch 2(A33, A34);
set Z8 = (EmptyBag 6) +* (4,8);
( ((EmptyBag 6) +* (0,8)) +* (0,0) = (EmptyBag 6) +* (0,0) & (EmptyBag 6) . 0 = 0 ) by FUNCT_7:34;
then Subst (((EmptyBag 6) +* (0,8)),0,((EmptyBag 6) +* (4,8))) = (EmptyBag 6) + ((EmptyBag 6) +* (4,8)) by FUNCT_7:35
.= (EmptyBag 6) +* (4,8) by PRE_POLY:53 ;
then A44: (Subst (((SgmX ((BagOrder 6),(Support q))) /. I),0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . ((EmptyBag 6) +* (4,8)) = (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (((EmptyBag 6) +* (0,8)) . 0)) . ((EmptyBag 6) +* (4,8)) by Th33, A29, A31
.= 1_ F_Real by A20, A43 ;
A45: for i being Nat st i in dom S holds
for b being bag of 6 st b in Support ((q . ((SgmX ((BagOrder 6),(Support q))) /. i)) * (Subst (((SgmX ((BagOrder 6),(Support q))) /. i),0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))) & b . 4 >= 8 holds
( i = I & b = (EmptyBag 6) +* (4,8) )

proof

let i be Nat; :: thesis:
assume A46: i in dom S ; :: thesis:
set Supi = (SgmX ((BagOrder 6),(Support q))) /. i;
let b be bag of 6; :: thesis:
assume A47: ( b in Support ((q . ((SgmX ((BagOrder 6),(Support q))) /. i)) * (Subst (((SgmX ((BagOrder 6),(Support q))) /. i),0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))) & b . 4 >= 8 ) ; :: thesis:
A48: ( (SgmX ((BagOrder 6),(Support q))) /. i = (SgmX ((BagOrder 6),(Support q))) . i & (SgmX ((BagOrder 6),(Support q))) . i in Support q ) by A46, A8, A5, PARTFUN1:def 6, FUNCT_1:def 3;
then A49: q . ((SgmX ((BagOrder 6),(Support q))) /. i) <> 0. F_Real by POLYNOM1:def 3;
A50: q . ((SgmX ((BagOrder 6),(Support q))) /. i) = (Jsqrt M) . (((SgmX ((BagOrder 6),(Support q))) /. i) | 4) by A48, A3;
A51: 4 -' 0 = 4 - 0 ;
((SgmX ((BagOrder 6),(Support q))) /. i) | 4 = (0,4) -cut ((SgmX ((BagOrder 6),(Support q))) /. i) by HILB10_2:3;
then reconsider Supi4 = ((SgmX ((BagOrder 6),(Support q))) /. i) | 4 as bag of 4 by A51;
A52: ( (2 (#) Supi4) +* (0,(Supi4 . 0)) in Bags 4 & Bags 4 = dom M ) by PRE_POLY:def 12, FUNCT_2:def 1;
set 2Supi4 = (2 (#) Supi4) +* (0,(Supi4 . 0));
Jsqrt M = JsqrtSeries M by Def13;
then (Jsqrt M) . Supi4 = M . ((2 (#) Supi4) +* (0,(Supi4 . 0))) by Def12;
then (2 (#) Supi4) +* (0,(Supi4 . 0)) in Support M by A52, A49, A50, COMPLFLD:7, POLYNOM1:def 3;
then A53: degree ((2 (#) Supi4) +* (0,(Supi4 . 0))) = 2 |^ (4 -' 1) by Def10;
consider g being FinSequence of REAL such that
A54: ( Sum ((2 (#) Supi4) +* (0,(Supi4 . 0))) = Sum g & g = ((2 (#) Supi4) +* (0,(Supi4 . 0))) * (canFS (support ((2 (#) Supi4) +* (0,(Supi4 . 0))))) ) by UPROOTS:def 3;
A55: for i being Nat st i in dom g holds
0 <= g . i by A54;
A56: ((2 (#) Supi4) +* (0,(Supi4 . 0))) . 0 <= 8

proof

A57: rng (canFS (support ((2 (#) Supi4) +* (0,(Supi4 . 0))))) = support ((2 (#) Supi4) +* (0,(Supi4 . 0))) by FUNCT_2:def 3;

per cases ;

suppose A58: 0 in support ((2 (#) Supi4) +* (0,(Supi4 . 0))) ; :: thesis:

then A59: ( 0 in rng (canFS (support ((2 (#) Supi4) +* (0,(Supi4 . 0))))) & rng (canFS (support ((2 (#) Supi4) +* (0,(Supi4 . 0))))) c= dom ((2 (#) Supi4) +* (0,(Supi4 . 0))) ) by PRE_POLY:37, A57;
consider d being object such that
A60: ( d in dom (canFS (support ((2 (#) Supi4) +* (0,(Supi4 . 0))))) & (canFS (support ((2 (#) Supi4) +* (0,(Supi4 . 0))))) . d = 0 ) by A58, A57, FUNCT_1:def 3;
reconsider d = d as Nat by A60;
( d in dom g & g . d = ((2 (#) Supi4) +* (0,(Supi4 . 0))) . 0 ) by A59, A60, A54, FUNCT_1:12, FUNCT_1:11;
hence ((2 (#) Supi4) +* (0,(Supi4 . 0))) . 0 <= 8 by A54, A53, A9, A55, MATRPROB:5; :: thesis:

end;

suppose not 0 in support ((2 (#) Supi4) +* (0,(Supi4 . 0))) ; :: thesis:

hence ((2 (#) Supi4) +* (0,(Supi4 . 0))) . 0 <= 8 by PRE_POLY:def 7; :: thesis:

end;

A61: ( 0 in Segm 4 & Segm 4 = dom (2 (#) Supi4) ) by NAT_1:44, PARTFUN1:def 2;
then A62: ((2 (#) Supi4) +* (0,(Supi4 . 0))) . 0 = Supi4 . 0 by FUNCT_7:31
.= ((SgmX ((BagOrder 6),(Support q))) /. i) . 0 by A61, FUNCT_1:49 ;
defpred S₂[ Nat] means for b being bag of 6 st (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ $1) . b <> 0. F_Real holds
b . 4 <= $1;
A63: S₂[ 0 ]

proof

let b be bag of 6; :: thesis:
assume A64: (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ 0) . b <> 0. F_Real ; :: thesis:
b = EmptyBag 6 by A64, POLYNOM1:25, A32;
hence b . 4 <= 0 ; :: thesis:

end;

A65: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume A66: S₂[i] ; :: thesis:
let b be bag of 6; :: thesis:
assume A67: (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (i + 1)) . b <> 0. F_Real ; :: thesis:
((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (i + 1) = (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i) *' ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) by Th29
.= ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) + ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) by POLYNOM1:26 ;
then (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (i + 1)) . b = (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b) + (((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b) by POLYNOM1:15;

per cases ) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real or ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real ) by A67;

suppose A68: ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real ; :: thesis:

end;

suppose A72: ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real ; :: thesis:

end;

proof

let x be object ; :: thesis:
assume A85: x in dom ((SgmX ((BagOrder 6),(Support q))) /. i) ; :: thesis:
reconsider x = x as Nat by A84, A85;

per cases ;

suppose x = 0 ; :: thesis:

hence ((SgmX ((BagOrder 6),(Support q))) /. i) . x = ((EmptyBag 6) +* (0,8)) . x by A82, A62, A56, XXREAL_0:1, A20; :: thesis:

end;

suppose A86: ( x <> 0 & x < 4 ) ; :: thesis:

then A87: x in Segm 4 by NAT_1:44;
((2 (#) Supi4) +* (0,(Supi4 . 0))) . x = ((EmptyBag 4) +* (0,8)) . x by A83, A62, Th19, A9, A53;
then A88: ((2 (#) Supi4) +* (0,(Supi4 . 0))) . x = (EmptyBag 4) . x by A86, FUNCT_7:32;
((2 (#) Supi4) +* (0,(Supi4 . 0))) . x = (2 (#) Supi4) . x by A86, FUNCT_7:32
.= 2 * (Supi4 . x) by VALUED_1:6 ;
then ( ((SgmX ((BagOrder 6),(Support q))) /. i) . x = 0 & 0 = (EmptyBag 6) . x & (EmptyBag 6) . x = ((EmptyBag 6) +* (0,8)) . x ) by A86, A87, A88, FUNCT_1:49, FUNCT_7:32;
hence ((SgmX ((BagOrder 6),(Support q))) /. i) . x = ((EmptyBag 6) +* (0,8)) . x ; :: thesis:

end;

suppose A89: x >= 4 ; :: thesis:

then ((EmptyBag 6) +* (0,8)) . x = (EmptyBag 6) . x by FUNCT_7:32;
hence ((SgmX ((BagOrder 6),(Support q))) /. i) . x = ((EmptyBag 6) +* (0,8)) . x by A89, A48, A2; :: thesis:

end;

then A90: (SgmX ((BagOrder 6),(Support q))) /. i = (EmptyBag 6) +* (0,8) by A84;
SgmX ((BagOrder 6),(Support q)) is one-to-one by POLYNOM2:18, PRE_POLY:10;
hence i = I by A29, A46, A8, A48, A90; :: thesis:
A91: (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ 8) . s <> 0. F_Real by A78, A79, Th33, A83;
defpred S₃[ Nat] means for b being bag of 6 st (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ $1) . b <> 0. F_Real holds
degree b = $1;
A92: S₃[ 0 ] by UPROOTS:11, POLYNOM1:25, A32;
A93: for i being Nat st S₃[i] holds
S₃[i + 1]

proof

let i be Nat; :: thesis:
assume A94: S₃[i] ; :: thesis:
let b be bag of 6; :: thesis:
assume A95: (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (i + 1)) . b <> 0. F_Real ; :: thesis:
((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (i + 1) = (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i) *' ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) by Th29
.= ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) + ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) by POLYNOM1:26 ;
then (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (i + 1)) . b = (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b) + (((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b) by POLYNOM1:15;

per cases ) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real or ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real ) by A95;

suppose A96: ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real ; :: thesis:

(Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i) = (- (1. F_Real)) * (((EmptyBag 6) +* (0,1)) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) by POLYRED:22;
then ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b = (- (1. F_Real)) * ((((EmptyBag 6) +* (0,1)) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b) by POLYNOM7:def 9;
then A97: (((EmptyBag 6) +* (0,1)) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real by A96;
then A98: (EmptyBag 6) +* (0,1) divides b by POLYRED:def 1;
then (((EmptyBag 6) +* (0,1)) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b = (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i) . (b -' ((EmptyBag 6) +* (0,1))) by POLYRED:def 1;
then A99: degree (b -' ((EmptyBag 6) +* (0,1))) = i by A94, A97;
reconsider z = 0 as Element of 6 by A19;
reconsider Z = {z} as Subset of 6 ;
(EmptyBag 6) +* (0,1) = ({z},1) -bag by Th12;
then A100: degree ((EmptyBag 6) +* (0,1)) = card Z by UPROOTS:13
.= 1 by CARD_1:30 ;
b = (b -' ((EmptyBag 6) +* (0,1))) + ((EmptyBag 6) +* (0,1)) by A98, PRE_POLY:47;
hence degree b = i + 1 by A99, A100, UPROOTS:15; :: thesis:

end;

suppose A101: ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real ; :: thesis:

(Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i) = (1. F_Real) * (((EmptyBag 6) +* (4,1)) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) by POLYRED:22;
then A102: ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b = (1. F_Real) * ((((EmptyBag 6) +* (4,1)) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b) by POLYNOM7:def 9;
then A103: (EmptyBag 6) +* (4,1) divides b by A101, POLYRED:def 1;
then (((EmptyBag 6) +* (4,1)) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b = (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i) . (b -' ((EmptyBag 6) +* (4,1))) by POLYRED:def 1;
then A104: degree (b -' ((EmptyBag 6) +* (4,1))) = i by A94, A102, A101;
reconsider z = 4 as Element of 6 by A19;
reconsider Z = {z} as Subset of 6 ;
(EmptyBag 6) +* (4,1) = ({z},1) -bag by Th12;
then A105: degree ((EmptyBag 6) +* (4,1)) = card Z by UPROOTS:13
.= 1 by CARD_1:30 ;
b = (b -' ((EmptyBag 6) +* (4,1))) + ((EmptyBag 6) +* (4,1)) by A103, PRE_POLY:47;
hence degree b = i + 1 by A104, A105, UPROOTS:15; :: thesis:

end;

for j being Nat holds S₃[j] from NAT_1:sch 2(A92, A93);
then A106: degree s = 8 by A91;
s . 4 = 8 by A81, A83, A47, A80, A79, XXREAL_0:1;
then A107: s = (EmptyBag 6) +* (4,8) by A106, Th19;
b = ((EmptyBag 6) +* (0,((EmptyBag 6) . 0))) + s by A90, A79, FUNCT_7:34;
then b = (EmptyBag 6) + s by FUNCT_7:35;
hence b = (EmptyBag 6) +* (4,8) by A107, PRE_POLY:53; :: thesis:

end;

A108: for i being Nat st i in dom S holds
for b being bag of 6 st b in Support ((q . ((SgmX ((BagOrder 6),(Support q))) /. i)) * (Subst (((SgmX ((BagOrder 6),(Support q))) /. i),0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))) holds
b . 5 = 0

proof

let i be Nat; :: thesis:
assume A109: i in dom S ; :: thesis:
set Supi = (SgmX ((BagOrder 6),(Support q))) /. i;
let b be bag of 6; :: thesis:
assume A110: b in Support ((q . ((SgmX ((BagOrder 6),(Support q))) /. i)) * (Subst (((SgmX ((BagOrder 6),(Support q))) /. i),0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))) ; :: thesis:
A111: ( (SgmX ((BagOrder 6),(Support q))) /. i = (SgmX ((BagOrder 6),(Support q))) . i & (SgmX ((BagOrder 6),(Support q))) . i in Support q ) by A5, A109, A8, PARTFUN1:def 6, FUNCT_1:def 3;
A112: 4 -' 0 = 4 - 0 ;
((SgmX ((BagOrder 6),(Support q))) /. i) | 4 = (0,4) -cut ((SgmX ((BagOrder 6),(Support q))) /. i) by HILB10_2:3;
then reconsider Supi4 = ((SgmX ((BagOrder 6),(Support q))) /. i) | 4 as bag of 4 by A112;
set 2Supi4 = (2 (#) Supi4) +* (0,(Supi4 . 0));
defpred S₂[ Nat] means for b being bag of 6 st (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ $1) . b <> 0. F_Real holds
b . 5 = 0 ;
A113: S₂[ 0 ]

proof

let b be bag of 6; :: thesis:
assume A114: (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ 0) . b <> 0. F_Real ; :: thesis:
b = EmptyBag 6 by A114, POLYNOM1:25, A32;
hence b . 5 = 0 ; :: thesis:

end;

A115: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume A116: S₂[i] ; :: thesis:
let b be bag of 6; :: thesis:
assume A117: (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (i + 1)) . b <> 0. F_Real ; :: thesis:
((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (i + 1) = (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i) *' ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) by Th29
.= ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) + ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) by POLYNOM1:26 ;
then (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ (i + 1)) . b = (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b) + (((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b) by POLYNOM1:15;

suppose A118: ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real ; :: thesis:

end;

suppose A123: ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) *' (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))) `^ i)) . b <> 0. F_Real ; :: thesis:

end;

end;

set PR = Polynom-Ring (6,F_Real);
defpred S₂[ Nat] means for i being Nat st $1 = i & i <= len S holds
for w being Polynomial of 6,F_Real st w = Sum (S | i) holds
( ( I <= i implies w . ((EmptyBag 6) +* (4,8)) = 1_ F_Real ) & ( i < I implies w . ((EmptyBag 6) +* (4,8)) = 0. F_Real ) & ( for b being bag of 6 st b in Support w & b <> (EmptyBag 6) +* (4,8) holds
b . 4 < 8 ) & ( for b being bag of 6 st b in Support w holds
b . 5 = 0 ) );
A132: S₂[ 0 ]

proof

let i be Nat; :: thesis:
assume A133: ( 0 = i & i <= len S ) ; :: thesis:
let w be Polynomial of 6,F_Real; :: thesis:
assume A134: w = Sum (S | i) ; :: thesis:
thus ( I <= i implies w . ((EmptyBag 6) +* (4,8)) = 1_ F_Real ) by A133, A29, FINSEQ_3:25; :: thesis:
S | i = <*> the carrier of (Polynom-Ring (6,F_Real)) by A133;
then A135: w = 0. (Polynom-Ring (6,F_Real)) by A134, RLVECT_1:43
.= 0_ (6,F_Real) by POLYNOM1:def 11 ;
hence ( i < I implies w . ((EmptyBag 6) +* (4,8)) = 0. F_Real ) by POLYNOM1:22; :: thesis:
thus for b being bag of 6 st b in Support w & b <> (EmptyBag 6) +* (4,8) holds
b . 4 < 8 :: thesis:

proof

let b be bag of 6; :: thesis:
assume b in Support w ; :: thesis:
then w . b <> 0. F_Real by POLYNOM1:def 3;
hence ( not b <> (EmptyBag 6) +* (4,8) or b . 4 < 8 ) by A135, POLYNOM1:22; :: thesis:

end;

thus for b being bag of 6 st b in Support w holds
b . 5 = 0 :: thesis:

proof

let b be bag of 6; :: thesis:
assume b in Support w ; :: thesis:
then w . b <> 0. F_Real by POLYNOM1:def 3;
hence b . 5 = 0 by A135, POLYNOM1:22; :: thesis:

end;

A136: ((EmptyBag 6) +* (4,8)) . 4 = 8 by A19, A18, FUNCT_7:31;
A137: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume A138: S₂[n] ; :: thesis:
let n1 be Nat; :: thesis:
assume A139: ( n1 = n + 1 & n1 <= len S ) ; :: thesis:
let w be Polynomial of 6,F_Real; :: thesis:
assume A140: w = Sum (S | n1) ; :: thesis:
reconsider w1 = Sum (S | n), Sn1 = S /. n1 as Polynomial of 6,F_Real by POLYNOM1:def 11;
A141: n1 in dom S by A139, FINSEQ_3:25, NAT_1:11;
then A142: ( S | n1 = (S | n) ^ <*(S . n1)*> & S . n1 = S /. n1 ) by A139, FINSEQ_5:10, PARTFUN1:def 6;
then A143: w = (Sum (S | n)) + (Sum <*(S /. n1)*>) by A140, RLVECT_1:41
.= (Sum (S | n)) + (S /. n1) by RLVECT_1:44
.= w1 + Sn1 by POLYNOM1:def 11 ;
A144: Sn1 = (q . ((SgmX ((BagOrder 6),(Support q))) /. n1)) * (Subst (((SgmX ((BagOrder 6),(Support q))) /. n1),0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) by A142, A7, A141;
A145: n < len S by A139, NAT_1:13;
A146: ( (EmptyBag 6) +* (4,8) in Bags 6 & Bags 6 = dom Sn1 ) by PRE_POLY:def 12, FUNCT_2:def 1;
thus ( I <= n1 implies w . ((EmptyBag 6) +* (4,8)) = 1_ F_Real ) :: thesis:

proof

assume A147: I <= n1 ; :: thesis:
A148: w . ((EmptyBag 6) +* (4,8)) = (w1 . ((EmptyBag 6) +* (4,8))) + (Sn1 . ((EmptyBag 6) +* (4,8))) by A143, POLYNOM1:15;

per cases by A147, XXREAL_0:1;

suppose A149: I = n1 ; :: thesis:

then n < I by A139, NAT_1:13;
then A150: w1 . ((EmptyBag 6) +* (4,8)) = 0. F_Real by A145, A138;
Sn1 . ((EmptyBag 6) +* (4,8)) = ((1. F_Real) * (Subst (((SgmX ((BagOrder 6),(Support q))) /. I),0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))) . ((EmptyBag 6) +* (4,8)) by A141, A149, A29, A31, A30, A7
.= (1. F_Real) * (1_ F_Real) by A44, POLYNOM7:def 9 ;
hence w . ((EmptyBag 6) +* (4,8)) = 1_ F_Real by A148, A150; :: thesis:

end;

suppose A151: I < n1 ; :: thesis:

then A152: I <= n by A139, NAT_1:13;
assume w . ((EmptyBag 6) +* (4,8)) <> 1_ F_Real ; :: thesis:
then Sn1 . ((EmptyBag 6) +* (4,8)) <> 0. F_Real by A148, A152, A145, A138;
then (EmptyBag 6) +* (4,8) in Support Sn1 by A146, POLYNOM1:def 3;
hence contradiction by A45, A144, A141, A136, A151; :: thesis:

end;

thus ( n1 < I implies w . ((EmptyBag 6) +* (4,8)) = 0. F_Real ) :: thesis:

proof

assume A153: ( n1 < I & w . ((EmptyBag 6) +* (4,8)) <> 0. F_Real ) ; :: thesis:
then n < I by NAT_1:13, A139;
then w1 . ((EmptyBag 6) +* (4,8)) = 0. F_Real by A145, A138;
then w . ((EmptyBag 6) +* (4,8)) = (0. F_Real) + (Sn1 . ((EmptyBag 6) +* (4,8))) by A143, POLYNOM1:15;
then (EmptyBag 6) +* (4,8) in Support Sn1 by A153, A146, POLYNOM1:def 3;
hence contradiction by A153, A45, A144, A141, A136; :: thesis:

end;

thus for b being bag of 6 st b in Support w & b <> (EmptyBag 6) +* (4,8) holds
b . 4 < 8 :: thesis:

proof

let b be bag of 6; :: thesis:
assume A154: ( b in Support w & b <> (EmptyBag 6) +* (4,8) ) ; :: thesis:
Support w c= (Support w1) \/ (Support Sn1) by A143, POLYNOM1:20;

per cases by XBOOLE_0:def 3, A154;

suppose b in Support w1 ; :: thesis:

hence b . 4 < 8 by A145, A154, A138; :: thesis:

end;

suppose b in Support Sn1 ; :: thesis:

hence b . 4 < 8 by A154, A141, A144, A45; :: thesis:

end;

let b be bag of 6; :: thesis:
assume A155: b in Support w ; :: thesis:
Support w c= (Support w1) \/ (Support Sn1) by A143, POLYNOM1:20;

per cases by XBOOLE_0:def 3, A155;

suppose b in Support w1 ; :: thesis:

hence b . 5 = 0 by A145, A138; :: thesis:

end;

suppose b in Support Sn1 ; :: thesis:

hence b . 5 = 0 by A141, A144, A108; :: thesis:

end;

set SU = Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))));
A156: S | (len S) = S ;
A157: for n being Nat holds S₂[n] from NAT_1:sch 2(A132, A137);
A158: I <= len S by A6, A29, FINSEQ_3:25;
A159: for b being bag of 6 st b in Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) holds
b . 4 <= 8 by A136, A157, A6, A156;
defpred S₃[ bag of 6, Element of F_Real] means ( ( ($1 . 4) + ($1 . 5) = 8 implies $2 = (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . ($1 +* (5,0)) ) & ( ($1 . 4) + ($1 . 5) <> 8 implies $2 = 0. F_Real ) );
A160: for x being Element of Bags 6 ex y being Element of F_Real st S₃[x,y]

proof

let x be Element of Bags 6; :: thesis:

per cases ) + (x . 5) = 8 or (x . 4) + (x . 5) <> 8 ) ;

suppose A161: (x . 4) + (x . 5) = 8 ; :: thesis:

take (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . (x +* (5,0)) ; :: thesis:
thus S₃[x,(Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . (x +* (5,0))] by A161; :: thesis:

end;

suppose A162: (x . 4) + (x . 5) <> 8 ; :: thesis:

take 0. F_Real ; :: thesis:
thus S₃[x, 0. F_Real] by A162; :: thesis:

end;

consider W being Function of (Bags 6),F_Real such that
A163: for x being Element of Bags 6 holds S₃[x,W . x] from FUNCT_2:sch 3(A160);
set SS = SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))));
A164: ( dom (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) = Bags 6 & Bags 6 = dom W ) by FUNCT_2:def 1;
BagOrder 6 linearly_orders Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) by POLYNOM2:18;
then A165: rng (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) = Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) by PRE_POLY:def 2;
reconsider SS = SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))))) as one-to-one FinSequence of Bags 6 by POLYNOM2:18, PRE_POLY:10;
deffunc H₁( object ) -> set = (SS /. $1) +* (5,(8 -' ((SS /. $1) . 4)));
consider SW being FinSequence such that
A166: len SW = len SS and
A167: for k being Nat st k in dom SW holds
SW . k = H₁(k) from FINSEQ_1:sch 2();
A168: dom SS = dom SW by A166, FINSEQ_3:29;
A169: rng SW c= Support W

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng SW ; :: thesis:
then consider z being object such that
A170: ( z in dom SW & SW . z = y ) by FUNCT_1:def 3;
reconsider z = z as Nat by A170;
A171: H₁(z) in Bags 6 by PRE_POLY:def 12;
A172: SW . z = H₁(z) by A170, A167;
A173: 6 = dom (SS /. z) by PARTFUN1:def 2;
A174: H₁(z) . 4 = (SS /. z) . 4 by FUNCT_7:32;
A175: H₁(z) . 5 = 8 -' ((SS /. z) . 4) by A19, A173, FUNCT_7:31;
( SS /. z = SS . z & SS . z in rng SS ) by A170, A168, FUNCT_1:def 3, PARTFUN1:def 6;
then H₁(z) . 5 = 8 - ((SS /. z) . 4) by A159, A165, A175, XREAL_1:233;
then (H₁(z) . 4) + (H₁(z) . 5) = 8 by A174;
then A176: W . H₁(z) = (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . (H₁(z) +* (5,0)) by A163, A171;
A177: ( SS /. z = SS . z & SS . z in rng SS ) by A170, A168, FUNCT_1:def 3, PARTFUN1:def 6;
then A178: (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . (SS /. z) <> 0. F_Real by POLYNOM1:def 3, A165;
A179: (SS /. z) . 5 = 0 by A157, A6, A156, A177, A165;
((SS /. z) +* (5,(8 -' ((SS /. z) . 4)))) +* (5,0) = (SS /. z) +* (5,0) by FUNCT_7:34
.= SS /. z by A179, FUNCT_7:35 ;
hence y in Support W by A176, A172, A170, A178, A171, A164, POLYNOM1:def 3; :: thesis:

end;

A180: Support W c= rng SW

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A181: z in Support W ; :: thesis:
then A182: ( z in dom W & W . z <> 0. F_Real ) by POLYNOM1:def 3;
reconsider z = z as bag of 6 by A181;
A183: z +* (5,0) in Bags 6 by PRE_POLY:def 12;
A184: S₃[z,W . z] by A181, A163;
z +* (5,0) in Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) by A164, A183, A182, A184, POLYNOM1:def 3;
then consider i being object such that
A185: ( i in dom SS & SS . i = z +* (5,0) ) by A165, FUNCT_1:def 3;
reconsider i = i as Nat by A185;
A186: SS . i = SS /. i by PARTFUN1:def 6, A185;
A187: (SS /. i) . 4 = z . 4 by A185, A186, FUNCT_7:32;
SW . i = (SS /. i) +* (5,(8 -' ((SS /. i) . 4))) by A167, A168, A185
.= (z +* (5,0)) +* (5,(8 -' ((SS /. i) . 4))) by A185, PARTFUN1:def 6
.= z +* (5,(8 -' ((SS /. i) . 4))) by FUNCT_7:34
.= z by A184, A181, POLYNOM1:def 3, FUNCT_7:35, A187 ;
hence z in rng SW by A185, A168, FUNCT_1:def 3; :: thesis:

end;

then A189: rng SW = Support W by A169, XBOOLE_0:def 10;
A190: SW is one-to-one

proof

let i1, i2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume A191: ( i1 in dom SW & i2 in dom SW & SW . i1 = SW . i2 ) ; :: thesis:
A192: ( SW . i1 = H₁(i1) & SW . i2 = H₁(i2) ) by A191, A167;
A193: ( 6 = dom (SS /. i1) & 6 = dom (SS /. i2) ) by PARTFUN1:def 2;
A194: ( SS /. i1 = SS . i1 & SS . i1 in rng SS ) by A191, A168, FUNCT_1:def 3, PARTFUN1:def 6;
A195: ( SS /. i2 = SS . i2 & SS . i2 in rng SS ) by A191, A168, FUNCT_1:def 3, PARTFUN1:def 6;
A196: ( SS /. i1 = SS . i1 & SS /. i2 = SS . i2 ) by A191, A168, PARTFUN1:def 6;
for x being object st x in 6 holds
(SS /. i1) . x = (SS /. i2) . x

proof

let j be object ; :: thesis:
assume A197: ( j in 6 & (SS /. i1) . j <> (SS /. i2) . j ) ; :: thesis:
A198: j in Segm 6 by A197;
then reconsider j = j as Nat ;
A199: ( (SS /. i1) . 5 = 0 & 0 = (SS /. i2) . 5 ) by A195, A194, A157, A6, A156, A165;
j < 5 + 1 by A198, NAT_1:44;
then A200: ( j <= 5 & j <> 5 ) by A199, NAT_1:13, A197;
H₁(i1) . j = (SS /. i1) . j by A200, FUNCT_7:32;
hence contradiction by A192, A191, A197, A200, FUNCT_7:32; :: thesis:

end;

then SS /. i1 = SS /. i2 by A193;
hence i1 = i2 by A196, A191, A168, FUNCT_1:def 4; :: thesis:

end;

reconsider SW = SW as one-to-one FinSequence of Bags 6 by A189, A190, FINSEQ_1:def 4;
reconsider W = W as Polynomial of 6,F_Real by A180, POLYNOM1:def 5;
reconsider RR = F_Real as Field ;
A202: dom (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) = Bags 6 by FUNCT_2:def 1;
rng W c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A203: ( y in rng W & not y in INT ) ; :: thesis:
then consider x being object such that
A204: ( x in dom W & W . x = y ) by FUNCT_1:def 3;
reconsider x = x as bag of 6 by A204;
A205: W . x <> 0 by A204, A203, INT_1:def 2;
A206: x +* (5,0) in Bags 6 by PRE_POLY:def 12;
(x . 4) + (x . 5) = 8 by A205, A163, A204;
then W . x = (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . (x +* (5,0)) by A163, A204;
then ( W . x in rng (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) & rng (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) c= INT ) by A206, A202, FUNCT_1:def 3, RELAT_1:def 19;
hence contradiction by A204, A203; :: thesis:

end;

then reconsider W = W as INT -valued Polynomial of 6,F_Real by RELAT_1:def 19;
take W ; :: thesis:
A207: len SW = card (Support W) by A189, FINSEQ_4:62;
reconsider SSU = Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))), WW = W as Polynomial of 6,RR ;
A208: for f being Function of 6,F_Real
for d being Element of F_Real st f . 5 <> 0 & d = (f . 4) / (f . 5) holds
eval (W,f) = ((power F_Real) . ((f /. 5),8)) * (eval ((Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))),(f +* (4,d))))

proof

let f be Function of 6,F_Real; :: thesis:
let divf be Element of F_Real; :: thesis:
assume that
A209: f . 5 <> 0 and
A210: divf = (f . 4) / (f . 5) ; :: thesis:
reconsider ff = f as Function of 6,RR ;
reconsider divff = divf as Element of RR ;
set ffd = ff +* (4,divff);
set fd = f +* (4,divf);
set P = (power RR) . ((ff /. 5),8);
set p = (power F_Real) . ((f /. 5),8);
reconsider SSU = Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))), WW = W as Polynomial of 6,RR ;
set PSU = ((power RR) . ((ff /. 5),8)) * SSU;
A211: ( dom (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) = Bags 6 & Bags 6 = dom (((power RR) . ((ff /. 5),8)) * SSU) ) by FUNCT_2:def 1;
dom f = 6 by FUNCT_2:def 1;
then f /. 5 = f . 5 by A19, PARTFUN1:def 6;
then A212: (power F_Real) . ((f /. 5),8) <> 0. F_Real by A209, Th6;
A213: Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) = Support (((power RR) . ((ff /. 5),8)) * SSU)

proof

thus Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) c= Support (((power RR) . ((ff /. 5),8)) * SSU) :: according to XBOOLE_0:def 10 :: thesis:

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume A214: u in Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) ; :: thesis:
reconsider u = u as bag of 6 by A214;
( ((power F_Real) . ((f /. 5),8)) * ((Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . u) = (((power RR) . ((ff /. 5),8)) * SSU) . u & (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . u <> 0. F_Real & u in dom (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) ) by A214, POLYNOM1:def 3, POLYNOM7:def 9;
hence u in Support (((power RR) . ((ff /. 5),8)) * SSU) by POLYNOM1:def 3, A211, A212; :: thesis:

end;

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume A215: u in Support (((power RR) . ((ff /. 5),8)) * SSU) ; :: thesis:
reconsider u = u as bag of 6 by A215;
( ((power F_Real) . ((f /. 5),8)) * ((Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . u) = (((power RR) . ((ff /. 5),8)) * SSU) . u & (((power RR) . ((ff /. 5),8)) * SSU) . u <> 0. F_Real & u in dom (((power RR) . ((ff /. 5),8)) * SSU) ) by A215, POLYNOM1:def 3, POLYNOM7:def 9;
then ( (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . u <> 0. F_Real & u in dom (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) ) by A211;
hence u in Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) by POLYNOM1:def 3; :: thesis:

end;

set SS = SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))));
consider y being FinSequence of RR such that
A216: ( len y = len (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) & eval ((((power RR) . ((ff /. 5),8)) * SSU),(ff +* (4,divff))) = Sum y ) and
A217: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (((((power RR) . ((ff /. 5),8)) * SSU) * (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))))))) /. i) * (eval (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. i),(ff +* (4,divff)))) by A213, POLYNOM2:def 4;
consider yW being FinSequence of RR such that
A218: ( len yW = card (Support WW) & eval (WW,ff) = Sum yW ) and
A219: for i being Nat st 1 <= i & i <= len yW holds
yW /. i = ((WW * SW) /. i) * (eval ((SW /. i),ff)) by A180, A169, XBOOLE_0:def 10, HILB10_2:24;
for j being Nat st 1 <= j & j <= len y holds
yW . j = y . j

proof

let j be Nat; :: thesis:
assume A220: ( 1 <= j & j <= len y ) ; :: thesis:
A221: j in NAT by ORDINAL1:def 12;
set SSj = (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j;
A222: ( j in dom (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) & j in dom SW & j in dom y & j in dom yW ) by A220, A216, A166, FINSEQ_3:25, A218, A207;
dom ((((power RR) . ((ff /. 5),8)) * SSU) * (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))))))) = dom (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) by RELAT_1:27, A165, A211;
then A223: ( ((((power RR) . ((ff /. 5),8)) * SSU) * (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))))))) /. j = ((((power RR) . ((ff /. 5),8)) * SSU) * (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))))))) . j & ((((power RR) . ((ff /. 5),8)) * SSU) * (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))))))) . j = (((power RR) . ((ff /. 5),8)) * SSU) . ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) . j) & (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) . j = (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j ) by A220, A216, FINSEQ_3:25, PARTFUN1:def 6, FUNCT_1:12;
dom (WW * SW) = dom SW by A164, A189, RELAT_1:27;
then A224: ( (WW * SW) /. j = (WW * SW) . j & (WW * SW) . j = WW . (SW . j) & SW . j = SW /. j ) by A220, A216, A166, FINSEQ_3:25, PARTFUN1:def 6, FUNCT_1:12;
A225: SW /. j = ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4))) by A224, A167, A220, A216, A166, FINSEQ_3:25;
A226: 6 = dom ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) by PARTFUN1:def 2;
A227: H₁(j) in Bags 6 by PRE_POLY:def 12;
A228: H₁(j) . 4 = ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4 by FUNCT_7:32;
A229: H₁(j) . 5 = 8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4) by A19, A226, FUNCT_7:31;
A230: ( (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j = (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) . j & (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) . j in rng (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) ) by A222, FUNCT_1:def 3, PARTFUN1:def 6;
then A231: 8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4) = 8 - (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4) by A159, A165, XREAL_1:233;
then (H₁(j) . 4) + (H₁(j) . 5) = 8 by A228, A229;
then A232: W . H₁(j) = (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . (H₁(j) +* (5,0)) by A163, A227;
A233: ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 5 = 0 by A230, A157, A6, A156, A165;
A234: H₁(j) +* (5,0) = ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0) by FUNCT_7:34
.= (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j by A233, FUNCT_7:35 ;
set SSj5 = ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0);
A235: (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4)))) +* (5,0) = ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0) by FUNCT_7:34;
A236: ( dom ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) = 6 & 6 = dom (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) ) by PARTFUN1:def 2;
then (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4)))) . 5 = 8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4) by A19, FUNCT_7:31;
then SW /. j = (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) + ((EmptyBag 6) +* (5,(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4)))) by A235, Th15, A225;
then A237: eval ((SW /. j),ff) = (eval ((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)),ff)) * (eval (((EmptyBag 6) +* (5,(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4)))),ff)) by POLYNOM2:16;
A238: eval (((EmptyBag 6) +* (5,(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4)))),ff) = (power RR) . ((ff . 5),(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4))) by A19, Th14;
A239: ( eval ((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)),(ff +* (4,divff))) = eval ((((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) +* (4,0)) + ((EmptyBag 6) +* (4,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4)))),(ff +* (4,divff))) & eval ((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)),ff) = eval ((((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) +* (4,0)) + ((EmptyBag 6) +* (4,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4)))),ff) ) by Th15;
A240: ( eval (((EmptyBag 6) +* (4,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))),(ff +* (4,divff))) = (power RR) . (((ff +* (4,divff)) . 4),((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4)) & eval (((EmptyBag 6) +* (4,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))),ff) = (power RR) . ((ff . 4),((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4)) ) by A19, Th14;
A241: ( dom ff = 6 & 6 = dom (ff +* (4,divff)) ) by PARTFUN1:def 2;
then A242: (ff +* (4,divff)) . 4 = divff by A19, FUNCT_7:31;
A243: ((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) +* (4,0)) . 4 = 0 by A236, A19, FUNCT_7:31;
A244: (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j = ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0) by A233, FUNCT_7:35;
A245: ( ff /. 5 = ff . 5 & ff /. 4 = ff . 4 ) by A241, A19, PARTFUN1:def 6;
A246: ( 8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4) in NAT & ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4 in NAT ) by ORDINAL1:def 12;
divff * (ff /. 5) = divf * (f /. 5)
.= divf * (f . 5) by A241, A19, PARTFUN1:def 6
.= f . 4 by XCMPLX_1:87, A209, A210 ;
then ((power RR) . (divff,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))) * ((power RR) . ((ff /. 5),((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))) = (power RR) . ((ff /. 4),((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4)) by A245, GROUP_1:52;
then A247: ((power RR) . ((ff /. 4),((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))) * ((power RR) . ((ff /. 5),(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4)))) = ((power RR) . (divff,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))) * (((power RR) . ((ff /. 5),((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))) * ((power RR) . ((ff /. 5),(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4))))) by GROUP_1:def 3
.= ((power RR) . (divff,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))) * ((power RR) . ((ff /. 5),((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4) + (8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4))))) by A246, A244, POLYNOM2:1
.= ((power RR) . (divff,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))) * ((power RR) . ((ff /. 5),8)) by A231 ;
A248: eval ((SW /. j),ff) = (eval ((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)),ff)) * ((power RR) . ((ff /. 5),(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4)))) by A241, A19, PARTFUN1:def 6, A237, A238
.= ((eval (((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) +* (4,0)),ff)) * (eval (((EmptyBag 6) +* (4,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))),ff))) * ((power RR) . ((ff /. 5),(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4)))) by A239, POLYNOM2:16
.= ((eval (((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) +* (4,0)),ff)) * ((power RR) . ((ff /. 4),((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4)))) * ((power RR) . ((ff /. 5),(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4)))) by A241, A19, PARTFUN1:def 6, A240
.= (eval (((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) +* (4,0)),ff)) * (((power RR) . ((ff /. 4),((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))) * ((power RR) . ((ff /. 5),(8 -' (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) . 4))))) by GROUP_1:def 3
.= (eval ((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (4,0)),(ff +* (4,divff)))) * ((eval (((EmptyBag 6) +* (4,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))),(ff +* (4,divff)))) * ((power RR) . ((ff /. 5),8))) by A240, A242, A243, Th18, A247, A244
.= ((eval ((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (4,0)),(ff +* (4,divff)))) * (eval (((EmptyBag 6) +* (4,((((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) +* (5,0)) . 4))),(ff +* (4,divff))))) * ((power RR) . ((ff /. 5),8)) by GROUP_1:def 3
.= (eval (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j),(ff +* (4,divff)))) * ((power RR) . ((ff /. 5),8)) by A239, POLYNOM2:16, A244 ;
A249: (WW * SW) /. j = (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j) by A234, A224, A167, A220, A216, A166, FINSEQ_3:25, A232;
A250: ((((power RR) . ((ff /. 5),8)) * SSU) * (SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))))))) /. j = ((power F_Real) . ((f /. 5),8)) * ((Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . ((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j)) by POLYNOM7:def 9, A223;
y /. j = (((power RR) . ((ff /. 5),8)) * ((WW * SW) /. j)) * (eval (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j),(ff +* (4,divff)))) by A249, A250, A217, A220, A221
.= ((WW * SW) /. j) * (((power RR) . ((ff /. 5),8)) * (eval (((SgmX ((BagOrder 6),(Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))))))))) /. j),(ff +* (4,divff))))) by GROUP_1:def 3
.= yW /. j by A216, A218, A219, A166, A207, A220, A248
.= yW . j by A222, PARTFUN1:def 6 ;
hence yW . j = y . j by A222, PARTFUN1:def 6; :: thesis:

end;

then eval ((((power RR) . ((ff /. 5),8)) * SSU),(ff +* (4,divff))) = eval (W,f) by A216, A218, A166, A207, FINSEQ_1:14;
hence eval (W,f) = ((power F_Real) . ((f /. 5),8)) * (eval ((Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))),(f +* (4,divf)))) by POLYNOM7:29; :: thesis:

end;

A251: ( 0 in Segm 6 & 1 in Segm 6 & 2 in Segm 6 & 3 in Segm 6 & 4 in Segm 6 & 5 in Segm 6 ) by NAT_1:44;
thus A252: for f being Function of 6,F_Real st f . 5 <> 0 holds
eval (W,f) = ((power F_Real) . ((f /. 5),8)) * (eval ((Jsqrt M),(@ <%((- (f . 0)) + ((f . 4) / (f . 5))),(f . 1),(f . 2),(f . 3)%>))) :: thesis:

proof

let f be Function of 6,F_Real; :: thesis:
assume A253: f . 5 <> 0 ; :: thesis:
reconsider divf = (f . 4) / (f . 5) as Element of F_Real by XREAL_0:def 1;
set fd = f +* (4,divf);
A254: eval (W,f) = ((power F_Real) . ((f /. 5),8)) * (eval ((Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))),(f +* (4,divf)))) by A253, A208;
A255: ( dom f = 6 & 6 = dom (f +* (4,divf)) ) by FUNCT_2:def 1;
A256: eval ((Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))),(f +* (4,divf))) = eval (q,((f +* (4,divf)) +* (0,(eval (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))),(f +* (4,divf))))))) by Th37, A251;
A257: eval (((EmptyBag 6) +* (4,1)),(f +* (4,divf))) = (power F_Real) . (((f +* (4,divf)) . 4),1) by A251, Th14
.= (power F_Real) . (divf,1) by A251, A255, FUNCT_7:31
.= divf by GROUP_1:50 ;
A258: ( (f +* (4,divf)) . 0 = f . 0 & f . 0 = f /. 0 ) by A251, A255, PARTFUN1:def 6, FUNCT_7:32;
A259: eval (((EmptyBag 6) +* (0,1)),(f +* (4,divf))) = (power F_Real) . (((f +* (4,divf)) . 0),1) by A251, Th14
.= f /. 0 by A258, GROUP_1:50 ;
A260: eval (((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))),(f +* (4,divf))) = (eval ((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))),(f +* (4,divf)))) + (eval ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))),(f +* (4,divf)))) by POLYNOM2:23
.= ((- (1. F_Real)) * (eval (((EmptyBag 6) +* (0,1)),(f +* (4,divf))))) + (eval ((Monom ((1. F_Real),((EmptyBag 6) +* (4,1)))),(f +* (4,divf)))) by POLYNOM7:13
.= ((- (1. F_Real)) * (eval (((EmptyBag 6) +* (0,1)),(f +* (4,divf))))) + ((1. F_Real) * (eval (((EmptyBag 6) +* (4,1)),(f +* (4,divf))))) by POLYNOM7:13
.= (- (f /. 0)) + divf by A259, A257
.= (- (f . 0)) + divf by A251, A255, PARTFUN1:def 6 ;
A261: Segm 4 c= Segm 6 by NAT_1:39;
A262: dom (((f +* (4,divf)) +* (0,((- (f . 0)) + divf))) | 4) = 4 by PARTFUN1:def 2, A261;
for x being object st x in 4 holds
(((f +* (4,divf)) +* (0,((- (f . 0)) + divf))) | 4) . x = (@ <%((- (f . 0)) + divf),(f . 1),(f . 2),(f . 3)%>) . x

proof

let x be object ; :: thesis:
assume A263: x in 4 ; :: thesis:
A264: 4 = Segm 4 ;
then reconsider x = x as Nat by A263;
( x < 4 & 4 = 3 + 1 ) by A263, A264, NAT_1:44;
then x <= 3 by NAT_1:13;
then not not x = 0 & ... & not x = 3 ;

per cases ;

suppose A265: x = 0 ; :: thesis:

then ((f +* (4,divf)) +* (0,((- (f . 0)) + divf))) . x = <%((- (f . 0)) + divf),(f . 1),(f . 2),(f . 3)%> . 0 by A261, A263, A255, FUNCT_7:31;
hence (((f +* (4,divf)) +* (0,((- (f . 0)) + divf))) | 4) . x = (@ <%((- (f . 0)) + divf),(f . 1),(f . 2),(f . 3)%>) . x by A265, A263, FUNCT_1:49; :: thesis:

end;

suppose A266: ( x = 1 or x = 2 or x = 3 ) ; :: thesis:

then ((f +* (4,divf)) +* (0,((- (f . 0)) + divf))) . x = (f +* (4,divf)) . x by FUNCT_7:32
.= <%((- (f . 0)) + divf),(f . 1),(f . 2),(f . 3)%> . x by A266, FUNCT_7:32 ;
hence (((f +* (4,divf)) +* (0,((- (f . 0)) + divf))) | 4) . x = (@ <%((- (f . 0)) + divf),(f . 1),(f . 2),(f . 3)%>) . x by A263, FUNCT_1:49; :: thesis:

end;

then ((f +* (4,divf)) +* (0,((- (f . 0)) + divf))) | 4 = @ <%((- (f . 0)) + divf),(f . 1),(f . 2),(f . 3)%> by PARTFUN1:def 2, A262;
hence eval (W,f) = ((power F_Real) . ((f /. 5),8)) * (eval ((Jsqrt M),(@ <%((- (f . 0)) + ((f . 4) / (f . 5))),(f . 1),(f . 2),(f . 3)%>))) by A254, A256, A260, A4; :: thesis:

end;

let f be INT -valued Function of 6,F_Real; :: thesis:
assume A267: ( f . 5 <> 0 & eval (W,f) = 0 ) ; :: thesis:
set N = (f . 5) gcd (f . 4);
consider g5, g4 being Integer such that
A268: ( f . 5 = ((f . 5) gcd (f . 4)) * g5 & f . 4 = ((f . 5) gcd (f . 4)) * g4 & g5,g4 are_coprime ) by A267, INT_2:23;
reconsider Nr = (f . 5) gcd (f . 4), g5r = g5, g4r = g4 as Element of F_Real by XREAL_0:def 1;
set g = (f +* (4,g4r)) +* (5,g5r);
reconsider g = (f +* (4,g4r)) +* (5,g5r) as Function of 6,F_Real ;
reconsider gg = g as Function of 6,RR ;
A269: (power F_Real) . ((f . 5),8) = (power F_Real) . ((Nr * g5r),8) by A268
.= ((power F_Real) . (Nr,8)) * ((power F_Real) . (g5r,8)) by GROUP_1:52 ;
A270: ( dom f = 6 & 6 = dom (f +* (4,g4)) & dom g = 6 & 6 = Segm 6 ) by PARTFUN1:def 2;
then A271: ( g . 0 = (f +* (4,g4)) . 0 & (f +* (4,g4)) . 0 = f . 0 & g . 1 = (f +* (4,g4)) . 1 & (f +* (4,g4)) . 1 = f . 1 & g . 2 = (f +* (4,g4)) . 2 & (f +* (4,g4)) . 2 = f . 2 & g . 3 = (f +* (4,g4)) . 3 & (f +* (4,g4)) . 3 = f . 3 & g . 4 = (f +* (4,g4)) . 4 & (f +* (4,g4)) . 4 = g4 & g . 5 = g5 ) by NAT_1:44, FUNCT_7:32, FUNCT_7:31;
rng g c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A272: y in rng g ; :: thesis:
consider x being object such that
A273: ( x in dom g & g . x = y ) by A272, FUNCT_1:def 3;
reconsider x = x as Nat by A273, A270;
( x < 6 & 6 = 5 + 1 ) by A273, A270, NAT_1:44;
then x <= 5 by NAT_1:13;
then not not x = 0 & ... & not x = 5 ;
hence y in INT by A271, A273, INT_1:def 2; :: thesis:

end;

then A274: g is INT -valued by RELAT_1:def 19;
A275: (power F_Real) . (Nr,8) <> 0. F_Real by A267, Th6;
A276: g . 5 <> 0 by A267, A271, A268;
A277: ( f /. 5 = f . 5 & g /. 5 = g . 5 ) by A270, NAT_1:44, PARTFUN1:def 6;
0. F_Real = ((power F_Real) . ((f /. 5),8)) * (eval ((Jsqrt M),(@ <%((- (f . 0)) + ((f . 4) / (f . 5))),(f . 1),(f . 2),(f . 3)%>))) by A267, A252
.= ((power F_Real) . ((f /. 5),8)) * (eval ((Jsqrt M),(@ <%((- (g . 0)) + ((g . 4) / (g . 5))),(g . 1),(g . 2),(g . 3)%>))) by A268, A267, XCMPLX_1:91, A271
.= (((power F_Real) . (Nr,8)) * ((power F_Real) . (g5r,8))) * (eval ((Jsqrt M),(@ <%((- (g . 0)) + ((g . 4) / (g . 5))),(g . 1),(g . 2),(g . 3)%>))) by A270, NAT_1:44, PARTFUN1:def 6, A269
.= ((power F_Real) . (Nr,8)) * (((power F_Real) . (g5r,8)) * (eval ((Jsqrt M),(@ <%((- (g . 0)) + ((g . 4) / (g . 5))),(g . 1),(g . 2),(g . 3)%>)))) ;
then A278: 0. F_Real = ((power F_Real) . (g5r,8)) * (eval ((Jsqrt M),(@ <%((- (g . 0)) + ((g . 4) / (g . 5))),(g . 1),(g . 2),(g . 3)%>))) by A275
.= ((power F_Real) . ((g /. 5),8)) * (eval ((Jsqrt M),(@ <%((- (g . 0)) + ((g . 4) / (g . 5))),(g . 1),(g . 2),(g . 3)%>))) by A270, NAT_1:44, FUNCT_7:31, A277
.= eval (W,g) by A276, A252 ;
set R8 = (EmptyBag 6) +* (4,8);
( (EmptyBag 6) +* (4,8) in Bags 6 & (EmptyBag 6) +* (4,8) in Bags 6 ) by PRE_POLY:def 12;
then A279: S₃[(EmptyBag 6) +* (4,8),W . ((EmptyBag 6) +* (4,8))] by A163;
A280: ( ((EmptyBag 6) +* (4,8)) . 5 = (EmptyBag 6) . 5 & (EmptyBag 6) . 5 = 0 ) by FUNCT_7:32;
((EmptyBag 6) +* (4,8)) +* (5,0) = ((EmptyBag 6) +* (5,((EmptyBag 6) . 5))) +* (4,8) by FUNCT_7:33
.= (EmptyBag 6) +* (4,8) by FUNCT_7:35 ;
then A281: W . ((EmptyBag 6) +* (4,8)) = 1_ F_Real by A280, A279, A18, A19, FUNCT_7:31, A158, A157, A6, A156;
set MZ = Monom ((1. F_Real),((EmptyBag 6) +* (4,8)));
set MZZ = Monom ((1. RR),((EmptyBag 6) +* (4,8)));
(Monom ((1. F_Real),((EmptyBag 6) +* (4,8)))) - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8)))) = 0_ (6,RR) by POLYNOM1:24;
then A282: W = ((Monom ((1. RR),((EmptyBag 6) +* (4,8)))) - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))) + WW by POLYNOM1:23
.= ((Monom ((1. RR),((EmptyBag 6) +* (4,8)))) + (- (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))) + WW by POLYNOM1:def 7
.= (Monom ((1. RR),((EmptyBag 6) +* (4,8)))) + ((- (Monom ((1. RR),((EmptyBag 6) +* (4,8))))) + WW) by POLYNOM1:21
.= (Monom ((1. F_Real),((EmptyBag 6) +* (4,8)))) + (W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))) by POLYNOM1:def 7 ;
set S = SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))));
BagOrder 6 linearly_orders Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))) by POLYNOM2:18;
then A283: rng (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) = Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))) by PRE_POLY:def 2;
consider Ry being FinSequence of RR such that
A284: ( len Ry = len (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) & eval ((WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))),gg) = Sum Ry ) and
A285: for i being Element of NAT st 1 <= i & i <= len Ry holds
Ry /. i = (((WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))) * (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))))))) /. i) * (eval (((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. i),gg)) by POLYNOM2:def 4;
defpred S₄[ Nat] means for i being Nat st i = $1 & $1 <= len (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) holds
ex s being Integer st s * (g . 5) = Sum (Ry | i);
A286: S₄[ 0 ]

proof

let i be Nat; :: thesis:
assume A287: ( i = 0 & 0 <= len (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) ) ; :: thesis:
take s = 0 ; :: thesis:
Ry | 0 = <*> the carrier of RR ;
then Sum (Ry | i) = 0. RR by A287, RLVECT_1:43;
hence s * (g . 5) = Sum (Ry | i) ; :: thesis:

end;

A288: term (Monom ((1. F_Real),((EmptyBag 6) +* (4,8)))) = (EmptyBag 6) +* (4,8) by POLYNOM7:10;
A289: (Monom ((1. F_Real),((EmptyBag 6) +* (4,8)))) . ((EmptyBag 6) +* (4,8)) = coefficient (Monom ((1. F_Real),((EmptyBag 6) +* (4,8)))) by POLYNOM7:10;
A290: for n being Nat st S₄[n] holds
S₄[n + 1]

proof

let n be Nat; :: thesis:
assume A291: S₄[n] ; :: thesis:
let n1 be Nat; :: thesis:
assume A292: ( n1 = n + 1 & n + 1 <= len (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) ) ; :: thesis:
n < len (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) by A292, NAT_1:13;
then consider s being Integer such that
A293: s * (g . 5) = Sum (Ry | n) by A291;
A294: n1 in dom (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) by A292, NAT_1:11, FINSEQ_3:25;
then A295: ( (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) . n1 in rng (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) & (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) . n1 = (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1 ) by FUNCT_1:def 3, PARTFUN1:def 6;
then A296: (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))) . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) <> 0. F_Real by A283, POLYNOM1:def 3;
A297: (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))) . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) = (WW + (- (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))) . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) by POLYNOM1:def 7
.= (WW . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1)) + ((- (Monom ((1. RR),((EmptyBag 6) +* (4,8))))) . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1)) by POLYNOM1:15
.= (WW . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1)) + (- ((Monom ((1. RR),((EmptyBag 6) +* (4,8)))) . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1))) by POLYNOM1:17 ;
A298: (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1 <> (EmptyBag 6) +* (4,8)

proof

assume (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1 = (EmptyBag 6) +* (4,8) ; :: thesis:
then (WW . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1)) + (- ((Monom ((1. RR),((EmptyBag 6) +* (4,8)))) . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1))) = (1_ F_Real) + (- (1_ F_Real)) by A281, A289, POLYNOM7:9;
hence contradiction by A296, A297; :: thesis:

end;

(Monom ((1. F_Real),((EmptyBag 6) +* (4,8)))) . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) = 0. F_Real by A288, A298, POLYNOM7:def 5;
then A299: WW . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) <> 0. F_Real by A295, A297, A283, POLYNOM1:def 3;
then A300: (((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) . 4) + (((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) . 5) = 8 by A163;
then A301: WW . ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) = (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) . (((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,0)) by A163;
A302: dom ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) = 6 by PARTFUN1:def 2;
A303: (((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,0)) . 4 = ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) . 4 by FUNCT_7:32;
A304: ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,0) <> (EmptyBag 6) +* (4,8)

proof

assume A305: ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,0) = (EmptyBag 6) +* (4,8) ; :: thesis:
consider j being object such that
A306: ( j in Segm 6 & ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) . j <> ((EmptyBag 6) +* (4,8)) . j ) by A302, A298, PARTFUN1:def 2;
reconsider j = j as Nat by A306;
A307: ((EmptyBag 6) +* (4,8)) . 5 = (EmptyBag 6) . 5 by FUNCT_7:32;
j < 5 + 1 by A306, NAT_1:44;
then ( j <= 5 & j <> 5 ) by NAT_1:13, A306, A305, A307, A300, A136, A303;
hence contradiction by A306, A305, FUNCT_7:32; :: thesis:

end;

((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,0) in Bags 6 by PRE_POLY:def 12;
then ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,0) in Support (Subst (q,0,((Monom ((- (1. F_Real)),((EmptyBag 6) +* (0,1)))) + (Monom ((1. F_Real),((EmptyBag 6) +* (4,1))))))) by A164, A299, A301, POLYNOM1:def 3;
then ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) . 5 <> 0 by A300, A303, A304, A157, A6, A156;
then reconsider O = (((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) . 5) - 1 as Nat ;
A308: (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1 = ((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,(O + 1)) by FUNCT_7:35
.= (((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,O)) + ((EmptyBag 6) +* (5,1)) by Th22 ;
A309: eval (((EmptyBag 6) +* (5,1)),gg) = (power F_Real) . ((gg . 5),1) by A251, Th14
.= g5r by GROUP_1:50, A271 ;
reconsider d1 = eval ((((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,O)),gg) as Integer by A274;
Bags 6 = dom (W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))) by FUNCT_2:def 1;
then dom ((W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))) * (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))))))) = dom (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) by A283, RELAT_1:27;
then ( ((W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))) * (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))))))) /. n1 = ((W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))) * (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))))))) . n1 & ((W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))) * (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))))))) . n1 in rng ((W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))) * (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))))))) & rng ((W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))) * (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))))))) c= INT ) by A294, PARTFUN1:def 6, FUNCT_1:def 3, RELAT_1:def 19;
then reconsider d2 = ((W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))) * (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))))))) /. n1 as Integer ;
reconsider E1 = eval ((((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,O)),g), E2 = eval (((EmptyBag 6) +* (5,1)),g) as Element of REAL ;
A310: eval (((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1),gg) = (eval ((((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1) +* (5,O)),g)) * (eval (((EmptyBag 6) +* (5,1)),g)) by A308, POLYNOM2:16;
A311: Ry /. n1 = (((WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))) * (SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8))))))))) /. n1) * (eval (((SgmX ((BagOrder 6),(Support (WW - (Monom ((1. RR),((EmptyBag 6) +* (4,8)))))))) /. n1),gg)) by A292, A284, A285, NAT_1:11
.= d2 * (E1 * E2) by BINOP_2:def 11, A310
.= (d2 * d1) * g5 by A309 ;
Ry | n1 = (Ry | n) ^ <*(Ry /. n1)*> by A292, A284, FINSEQ_5:82;
then Sum (Ry | n1) = (Sum (Ry | n)) + (Sum <*(Ry /. n1)*>) by RLVECT_1:41;
then Sum (Ry | n1) = the addF of RR . ((Sum (Ry | n)),(Ry /. n1)) by RLVECT_1:44
.= (s * (g . 5)) + ((d2 * d1) * g5) by A311, A293, BINOP_2:def 9
.= (g . 5) * (s + (d2 * d1)) by A271 ;
hence ex s being Integer st s * (g . 5) = Sum (Ry | n1) ; :: thesis:

end;

for n being Nat holds S₄[n] from NAT_1:sch 2(A286, A290);
then consider s being Integer such that
A312: s * (g . 5) = Sum (Ry | (len Ry)) by A284;
A313: eval (((EmptyBag 6) +* (4,8)),g) = (power F_Real) . ((g . 4),8) by A251, Th14
.= g4 |^ 8 by NIVEN:7, A271 ;
A314: eval ((Monom ((1. F_Real),((EmptyBag 6) +* (4,8)))),g) = (1. F_Real) * (eval (((EmptyBag 6) +* (4,8)),g)) by POLYNOM7:13
.= g4 |^ 8 by A313 ;
eval (W,g) = (eval ((Monom ((1. F_Real),((EmptyBag 6) +* (4,8)))),g)) + (eval ((W - (Monom ((1. F_Real),((EmptyBag 6) +* (4,8))))),g)) by A282, POLYNOM2:23
.= (s * (g . 5)) + (g4 |^ 8) by A312, A284, A314 ;
then A315: g5 * (- s) = g4 |^ 8 by A278, A271;
defpred S₅[ Nat] means ( g5 divides g4 |^ $1 implies g5 divides g4 );
A316: S₅[ 0 ]

proof

A317: g4 |^ 0 = 1 by NEWTON:4;
assume g5 divides g4 |^ 0 ; :: thesis:
then ( g5 = 1 or g5 = - 1 ) by A317, INT_2:13;
hence g5 divides g4 by INT_2:12; :: thesis:

end;

A318: for j being Nat st S₅[j] holds
S₅[j + 1]

proof

let j be Nat; :: thesis:
assume A319: ( S₅[j] & g5 divides g4 |^ (j + 1) ) ; :: thesis:
then g5 divides g4 * (g4 |^ j) by NEWTON:6;
hence g5 divides g4 by A319, A268, INT_2:25; :: thesis:

end;

for j being Nat holds S₅[j] from NAT_1:sch 2(A316, A318);
then ( g5 divides g4 & g5 divides g5 * 1 ) by A315, INT_1:def 3;
then g5 divides g5 gcd g4 by INT_2:22;
then g5 divides 1 by A268, INT_2:def 3;
then ( g5 = 1 or g5 = - 1 ) by INT_2:13;
then ( f . 4 = (f . 5) * (- g4) or f . 4 = (f . 5) * g4 ) by A268;
hence f . 5 divides f . 4 by INT_1:def 3; :: thesis: