let R1, R2 be Ring; :: thesis: for phi being Function of R1,R2 st phi is linear holds
phi . (1. R1) = 1. R2
let phi be Function of R1,R2; :: thesis: ( phi is linear implies phi . (1. R1) = 1. R2 )
assume A1: phi is linear ; :: thesis: phi . (1. R1) = 1. R2
thus phi . (1. R1) = phi . (1_ R1)
.= 1_ R2 by A1, GROUP_1:def 13
.= 1. R2 ; :: thesis: verum