let K be Field; :: thesis: for F being K -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
F, embField f are_isomorphic
let F be K -monomorphic Field; :: thesis: for f being Monomorphism of K,F st K,F are_disjoint holds
F, embField f are_isomorphic
let f be Monomorphism of K,F; :: thesis: ( K,F are_disjoint implies F, embField f are_isomorphic )
assume AS: K,F are_disjoint ; :: thesis: F, embField f are_isomorphic
set g = emb_iso f;
( emb_iso f is unity-preserving & emb_iso f is additive & emb_iso f is multiplicative ) by AS, Th11, Th12;
then emb_iso f is isomorphism by AS, Th13, MOD_4:def 12;
hence F, embField f are_isomorphic by QUOFIELD:def 23; :: thesis: verum