consider G, H being strict Element of V such that
A1: F is strict Morphism of G,H by Def23;
reconsider F9 = F as Morphism of G,H by A1;
dom F9 = G by Def12;
hence dom F is strict Element of V ; :: thesis: verum