let L be Field; 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; 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; ( 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 )
; 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))
; verum