set g = emb_iso f;
set R = embField f;
1. (embField f) = 1. K by defemb;
then 1. (embField f) in K ;
then (emb_iso f) . (1_ (embField f)) = f . (1. (embField f)) by defiso
.= f . (1_ K) by defemb
.= 1_ F by GROUP_1:def 13 ;
hence emb_iso f is unity-preserving ; :: thesis: verum