let R be Ring; for E being R -homomorphic Ring
for K being Subring of R
for f being Function of R,E
for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds
g is unity-preserving
let E be R -homomorphic Ring; for K being Subring of R
for f being Function of R,E
for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds
g is unity-preserving
let K be Subring of R; for f being Function of R,E
for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds
g is unity-preserving
let f be Function of R,E; for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds
g is unity-preserving
let g be Function of K,E; ( g = f | the carrier of K & f is unity-preserving implies g is unity-preserving )
assume that
A1:
g = f | the carrier of K
and
A2:
f is unity-preserving
; g is unity-preserving
thus g . (1_ K) =
f . (1_ K)
by A1, FUNCT_1:49
.=
1_ E
by A2, C0SP1:def 3
; GROUP_1:def 13 verum