let F be Field; :: thesis: for E being F -homomorphic Field
for K being Subfield of F
for f being Function of F,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 F -homomorphic Field; :: thesis: for K being Subfield of F
for f being Function of F,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 Subfield of F; :: thesis: for f being Function of F,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 F,E; :: thesis: 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; :: thesis: ( 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 ; :: thesis: g is unity-preserving
thus g . (1_ K) = f . (1_ K) by A1, FUNCT_1:49
.= 1_ E by A2, EC_PF_1:def 1 ; :: according to GROUP_1:def 13 :: thesis: verum