set M = { [K,g] where K is Element of SubFields E, g is Function of K,L : ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = K & g1 = g & g1 is monomorphism & g1 is f -extending ) } ;
set K1 = doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #);
H: doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) == F by lemug1;
then F is Subfield of doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) by FIELD_7:def 2;
then reconsider K1 = doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) as FieldExtension of F by FIELD_4:7;
J: F is Subfield of E by FIELD_4:7;
K1 is Subfield of F by H, FIELD_7:def 2;
then K1 is Subfield of E by J, EC_PF_1:5;
then reconsider K = K1 as Element of SubFields E by subfie;
reconsider g = f as Function of K,L ;
reconsider g1 = f as Function of K1,L ;
B: g1 is f -extending ;

C: now :: thesis: for x, y being Element of K1 holds g1 . (x + y) = (g1 . x) + (g1 . y)

let x, y be Element of K1; :: thesis: g1 . (x + y) = (g1 . x) + (g1 . y)
reconsider a = x, b = y as Element of F ;
thus g1 . (x + y) = f . (a + b)
.= (g1 . x) + (g1 . y) by VECTSP_1:def 20 ; :: thesis: verum

end;

D: now :: thesis: for x, y being Element of K1 holds g1 . (x * y) = (g1 . x) * (g1 . y)

let x, y be Element of K1; :: thesis: g1 . (x * y) = (g1 . x) * (g1 . y)
reconsider a = x, b = y as Element of F ;
thus g1 . (x * y) = f . (a * b)
.= (g1 . x) * (g1 . y) by GROUP_6:def 6 ; :: thesis: verum

end;

g1 . (1_ K1) = f . (1_ F)
.= 1_ L by GROUP_1:def 13 ;
then ( g1 is additive & g1 is multiplicative & g1 is unity-preserving ) by C, D;
then [K,g] in { [K,g] where K is Element of SubFields E, g is Function of K,L : ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = K & g1 = g & g1 is monomorphism & g1 is f -extending ) } by B;
hence { [K,g] where K is Element of SubFields E, g is Function of K,L : ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = K & g1 = g & g1 is monomorphism & g1 is f -extending ) } is non empty set ; :: thesis: verum