let L be Field; :: thesis: for p being rational_function of L
for x being Element of L st eval ((p `2),x) <> 0. L holds
eval ((NormRationalFunction p),x) = eval (p,x)
let p be rational_function of L; :: thesis: for x being Element of L st eval ((p `2),x) <> 0. L holds
eval ((NormRationalFunction p),x) = eval (p,x)
let x be Element of L; :: thesis: ( eval ((p `2),x) <> 0. L implies eval ((NormRationalFunction p),x) = eval (p,x) )
assume A1: eval ((p `2),x) <> 0. L ; :: thesis: eval ((NormRationalFunction p),x) = eval (p,x)
set np = NormRationalFunction p;
A2: (1. L) / (LC (p `2)) <> 0. L ;
thus eval ((NormRationalFunction p),x) = (eval ((((1. L) / (LC (p `2))) * (p `1)),x)) * ((eval (((NormRationalFunction p) `2),x)) ")
.= (eval ((((1. L) / (LC (p `2))) * (p `1)),x)) * ((eval ((((1. L) / (LC (p `2))) * (p `2)),x)) ")
.= (((1. L) / (LC (p `2))) * (eval ((p `1),x))) * ((eval ((((1. L) / (LC (p `2))) * (p `2)),x)) ") by POLYNOM5:30
.= (((1. L) / (LC (p `2))) * (eval ((p `1),x))) * ((((1. L) / (LC (p `2))) * (eval ((p `2),x))) ") by POLYNOM5:30
.= (((1. L) / (LC (p `2))) * (eval ((p `1),x))) * ((((1. L) / (LC (p `2))) ") * ((eval ((p `2),x)) ")) by A1, VECTSP_2:11
.= (eval ((p `1),x)) * (((1. L) / (LC (p `2))) * ((((1. L) / (LC (p `2))) ") * ((eval ((p `2),x)) "))) by GROUP_1:def 3
.= (eval ((p `1),x)) * ((((1. L) / (LC (p `2))) * (((1. L) / (LC (p `2))) ")) * ((eval ((p `2),x)) ")) by GROUP_1:def 3
.= (eval ((p `1),x)) * ((1. L) * ((eval ((p `2),x)) ")) by A2, VECTSP_1:def 10
.= eval (p,x) by VECTSP_1:def 8 ; :: thesis: verum