let F be Field; :: thesis: for Z being set ex E being Field st
( E,F are_isomorphic & the carrier of E /\ ( the carrier of F \/ Z) = {} )
let Z be set ; :: thesis: ex E being Field st
( E,F are_isomorphic & the carrier of E /\ ( the carrier of F \/ Z) = {} )
set r = the Renaming of the carrier of F,Z;
take E = RenField the Renaming of the carrier of F,Z; :: thesis: ( E,F are_isomorphic & the carrier of E /\ ( the carrier of F \/ Z) = {} )
the Renaming of the carrier of F,Z " is linear by thiso;
then the Renaming of the carrier of F,Z " is isomorphism by thiso, MOD_4:def 12;
hence E,F are_isomorphic ; :: thesis: the carrier of E /\ ( the carrier of F \/ Z) = {}
rng the Renaming of the carrier of F,Z = the carrier of E by defrf;
hence the carrier of E /\ ( the carrier of F \/ Z) = {} by defr; :: thesis: verum