consider G, H being strict Element of V such that
A2: F is strict Morphism of G,H by Def7;
reconsider F9 = F as Morphism of G,H by A2;
cod F9 = H by MOD_2:def 8;
hence cod F is Element of V ; :: thesis: verum