theorem Lm49: :: RINGFRAC:31

for A being non degenerated commutative Ring
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)