theorem :: ENS_1:26

for V being non empty set
for f being Morphism of (Ens V) holds
( dom f = dom (@ f) & cod f = cod (@ f) ) by Def9, Def10;