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

( 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