let R be Ring; :: thesis: for S being RingExtension of R
for a being Element of S
for p, q being Polynomial of R holds Ext_eval ((p - q),a) = (Ext_eval (p,a)) - (Ext_eval (q,a))
let S be RingExtension of R; :: thesis: for a being Element of S
for p, q being Polynomial of R holds Ext_eval ((p - q),a) = (Ext_eval (p,a)) - (Ext_eval (q,a))
let a be Element of S; :: thesis: for p, q being Polynomial of R holds Ext_eval ((p - q),a) = (Ext_eval (p,a)) - (Ext_eval (q,a))
let p, q be Polynomial of R; :: thesis: Ext_eval ((p - q),a) = (Ext_eval (p,a)) - (Ext_eval (q,a))
R is Subring of S by FIELD_4:def 1;
hence Ext_eval ((p - q),a) = (Ext_eval (p,a)) + (Ext_eval ((- q),a)) by ALGNUM_1:15
.= (Ext_eval (p,a)) - (Ext_eval (q,a)) by exevalminus ;
:: thesis: verum