let A be non degenerated commutative Ring; :: thesis: for S being non empty multiplicatively-closed without_zero Subset of A
for a, b being Element of A holds (canHom S) . (a - b) = ((canHom S) . a) - ((canHom S) . b)
let S be non empty multiplicatively-closed without_zero Subset of A; :: thesis: for a, b being Element of A holds (canHom S) . (a - b) = ((canHom S) . a) - ((canHom S) . b)
let a, b be Element of A; :: thesis: (canHom S) . (a - b) = ((canHom S) . a) - ((canHom S) . b)
thus (canHom S) . (a - b) = ((canHom S) . a) + ((canHom S) . (- b)) by VECTSP_1:def 20
.= ((canHom S) . a) - ((canHom S) . b) by RING_2:7 ; :: thesis: verum