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

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