consider G, H being strict Element of V such that
A1: F is strict Morphism of G,H by Def7;
reconsider F' = F as Morphism of G,H by A1;
dom F' = G by MOD_2:def 11;
hence dom F is Element of V ; :: thesis: verum