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 multiplicative holds
g is multiplicative
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 multiplicative holds
g is multiplicative
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 multiplicative holds
g is multiplicative
let f be Function of F,E; :: thesis: for g being Function of K,E st g = f | the carrier of K & f is multiplicative holds
g is multiplicative
let g be Function of K,E; :: thesis: ( g = f | the carrier of K & f is multiplicative implies g is multiplicative )
assume that
A1: g = f | the carrier of K and
A2: f is multiplicative ; :: thesis: g is multiplicative
let x, y be Element of K; :: according to GROUP_6:def 6 :: thesis: g . (x * y) = (g . x) * (g . y)
the carrier of K c= the carrier of F by EC_PF_1:def 1;
then reconsider x1 = x, y1 = y as Element of F ;
A3: x * y = ( the multF of F || the carrier of K) . (x,y) by EC_PF_1:def 1
.= x1 * y1 by Th1 ;
thus g . (x * y) = f . (x * y) by A1, FUNCT_1:49
.= (f . x1) * (f . y1) by A2, A3
.= (g . x) * (f . y1) by A1, FUNCT_1:49
.= (g . x) * (g . y) by A1, FUNCT_1:49 ; :: thesis: verum