let K be Field; :: thesis: for K1 being Subfield of K
for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & y = y1 holds
x * y = x1 * y1
let K1 be Subfield of K; :: thesis: for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & y = y1 holds
x * y = x1 * y1
let x, y be Element of K; :: thesis: for x1, y1 being Element of K1 st x = x1 & y = y1 holds
x * y = x1 * y1
let x1, y1 be Element of K1; :: thesis: ( x = x1 & y = y1 implies x * y = x1 * y1 )
set C = the carrier of K;
set C1 = the carrier of K1;
the multF of K1 = the multF of K || the carrier of K1 by EC_PF_1:def 1;
hence ( x = x1 & y = y1 implies x * y = x1 * y1 ) by FUNCT_1:49, ZFMISC_1:87; :: thesis: verum