set F = F_Rat ;
set KR = KroneckerField (F_Rat,p);
X: ( [#] F_Rat = the carrier of F_Rat & [#] (KroneckerField (F_Rat,p)) = the carrier of (KroneckerField (F_Rat,p)) ) ;
the carrier of F_Rat /\ the carrier of (KroneckerField (F_Rat,p)) = {} by Disj2;
hence ( embField (emb p) is add-associative & embField (emb p) is right_complementable & embField (emb p) is associative & embField (emb p) is distributive & embField (emb p) is almost_left_invertible ) by X, FIELD_2:12, FIELD_2:def 1; :: thesis: verum