let L be Field; :: thesis: for p, q being rational_function of L
for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds
eval ((p + q),x) = (eval (p,x)) + (eval (q,x))
let p, q be rational_function of L; :: thesis: for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds
eval ((p + q),x) = (eval (p,x)) + (eval (q,x))
let x be Element of L; :: thesis: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L implies eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) )
assume A1: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L ) ; :: thesis: eval ((p + q),x) = (eval (p,x)) + (eval (q,x))
thus eval ((p + q),x) = (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * ((eval (((p + q) `2),x)) ")
.= (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * ((eval (((p `2) *' (q `2)),x)) ")
.= (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * (((eval ((p `2),x)) * (eval ((q `2),x))) ") by POLYNOM4:24
.= (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by A1, VECTSP_2:11
.= ((eval (((p `1) *' (q `2)),x)) + (eval (((p `2) *' (q `1)),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by POLYNOM4:19
.= ((eval (((p `1) *' (q `2)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by VECTSP_1:def 3
.= (((eval ((p `1),x)) * (eval ((q `2),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by POLYNOM4:24
.= ((eval ((p `1),x)) * ((eval ((q `2),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by GROUP_1:def 3
.= ((eval ((p `1),x)) * (((eval ((q `2),x)) * ((eval ((q `2),x)) ")) * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by GROUP_1:def 3
.= ((eval ((p `1),x)) * ((1. L) * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by A1, VECTSP_1:def 10
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")))
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + (((eval ((p `2),x)) * (eval ((q `1),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by POLYNOM4:24
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval ((q `1),x)) * ((eval ((p `2),x)) * (((eval ((p `2),x)) ") * ((eval ((q `2),x)) ")))) by GROUP_1:def 3
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval ((q `1),x)) * (((eval ((p `2),x)) * ((eval ((p `2),x)) ")) * ((eval ((q `2),x)) "))) by GROUP_1:def 3
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval ((q `1),x)) * ((1. L) * ((eval ((q `2),x)) "))) by A1, VECTSP_1:def 10
.= (eval (p,x)) + (eval (q,x)) ; :: thesis: verum