let L be Field; :: thesis: for p being rational_function of L
for x being Element of L holds
( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
let p be rational_function of L; :: thesis: for x being Element of L holds
( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
let x be Element of L; :: thesis: ( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
assume AS1: eval ((p `2),x) <> 0. L ; :: thesis: ( x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
assume AS: not x is_a_common_root_of p `1 ,p `2 ; :: thesis: eval ((NF p),x) = eval (p,x)

per cases ( p is zero or not p is zero ) ;

suppose H: p is zero ; :: thesis: eval ((NF p),x) = eval (p,x)

then H1: p `1 = 0_. L by defzerrat;
H2: NF p = 0._ L by H, defNF;
thus eval (p,x) = (0. L) * ((eval ((p `2),x)) ") by H1, POLYNOM4:17
.= 0. L by VECTSP_1:7
.= eval ((NF p),x) by H2, ev0 ; :: thesis: verum

end;

suppose not p is zero ; :: thesis: eval ((NF p),x) = eval (p,x)

then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
H: ( p = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF p = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of p `1 ,p `2 & f . i = rpoly (1,x) ) ) ) ) by defNF;
H1: p `1 = z2 *' (z1 `1) by H, XTUPLE_0:def 2;
H2: p `2 = z2 *' (z1 `2) by H, XTUPLE_0:def 3;

H3: now :: thesis: not eval (z2,x) = 0. L

assume A: eval (z2,x) = 0. L ; :: thesis: contradiction
eval ((z2 *' (z1 `1)),x) = (eval (z2,x)) * (eval ((z1 `1),x)) by POLYNOM4:24
.= 0. L by A, VECTSP_1:7 ;
then B: x is_a_root_of p `1 by H1, POLYNOM5:def 6;
eval ((z2 *' (z1 `2)),x) = (eval (z2,x)) * (eval ((z1 `2),x)) by POLYNOM4:24
.= 0. L by A, VECTSP_1:7 ;
then x is_a_root_of p `2 by H2, POLYNOM5:def 6;
hence contradiction by AS, B, root1; :: thesis: verum

end;

H6: now :: thesis: not eval ((z1 `2),x) = 0. L

assume eval ((z1 `2),x) = 0. L ; :: thesis: contradiction
then 0. L = (eval (z2,x)) * (eval ((z1 `2),x)) by VECTSP_1:7
.= eval ((z2 *' (z1 `2)),x) by POLYNOM4:24 ;
hence contradiction by H, XTUPLE_0:def 3, AS1; :: thesis: verum

end;

eval (p,x) = (eval ((z2 *' (z1 `1)),x)) * ((eval ((z2 *' (z1 `2)),x)) ") by H, XTUPLE_0:def 3, H1
.= ((eval (z2,x)) * (eval ((z1 `1),x))) * ((eval ((z2 *' (z1 `2)),x)) ") by POLYNOM4:24
.= ((eval (z2,x)) * (eval ((z1 `1),x))) * (((eval (z2,x)) * (eval ((z1 `2),x))) ") by POLYNOM4:24
.= ((eval (z2,x)) * (eval ((z1 `1),x))) * (((eval ((z1 `2),x)) ") * ((eval (z2,x)) ")) by H3, H6, VECTSP_2:11
.= (eval (z2,x)) * ((eval ((z1 `1),x)) * (((eval ((z1 `2),x)) ") * ((eval (z2,x)) "))) by GROUP_1:def 3
.= (eval (z2,x)) * (((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) * ((eval (z2,x)) ")) by GROUP_1:def 3
.= ((eval (z2,x)) * ((eval (z2,x)) ")) * ((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) by GROUP_1:def 3
.= (1. L) * ((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) by H3, VECTSP_1:def 10
.= eval (z1,x) by VECTSP_1:def 8 ;
hence eval ((NF p),x) = eval (p,x) by H, H6, ev4; :: thesis: verum

end;

end;