consider G, H being Element of V such that
A1: G <= H and
A2: F is Morphism of G,H by Def17;
reconsider F9 = F as Morphism of G,H by A2;
dom F9 = G by A1, Def8;
hence dom F is Element of V ; :: thesis: verum