theorem Th1: :: MATGRP_0:1
for R1, R2 being Ring
for phi being Function of R1,R2 st phi is linear holds
phi . (1. R1) = 1. R2