theorem thisofield: :: FIELD_5:29

for F being Field
for Z being set ex E being Field st
( E,F are_isomorphic & the carrier of E /\ ( the carrier of F \/ Z) = {} )