let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -monomorphic Field
for h being Monomorphism of F1,F2
for p being Element of the carrier of (Polynom-Ring F1) holds (PolyHom h) . (- p) = - ((PolyHom h) . p)
let F2 be F1 -homomorphic F1 -monomorphic Field; :: thesis: for h being Monomorphism of F1,F2
for p being Element of the carrier of (Polynom-Ring F1) holds (PolyHom h) . (- p) = - ((PolyHom h) . p)
let h be Monomorphism of F1,F2; :: thesis: for p being Element of the carrier of (Polynom-Ring F1) holds (PolyHom h) . (- p) = - ((PolyHom h) . p)
let p be Element of the carrier of (Polynom-Ring F1); :: thesis: (PolyHom h) . (- p) = - ((PolyHom h) . p)
((PolyHom h) . p) + ((PolyHom h) . (- p)) = (PolyHom h) . (p + (- p)) by FIELD_1:24
.= (PolyHom h) . (0. (Polynom-Ring F1)) by RLVECT_1:5
.= (PolyHom h) . (0_. F1) by POLYNOM3:def 10
.= 0_. F2 by FIELD_1:22
.= 0. (Polynom-Ring F2) by POLYNOM3:def 10 ;
hence (PolyHom h) . (- p) = - ((PolyHom h) . p) by RLVECT_1:6; :: thesis: verum