set F = Z/ n;
set KR = KroneckerField ((Z/ n),p);
X: ( [#] (Z/ n) = the carrier of (Z/ n) & [#] (KroneckerField ((Z/ n),p)) = the carrier of (KroneckerField ((Z/ n),p)) ) ;
the carrier of (Z/ n) /\ the carrier of (KroneckerField ((Z/ n),p)) = {} by Disj1;
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