reconsider G9 = G as strict Element of V by Def15;
ID G9 is strict Element of Morphs V by Def23;
hence ID G is strict Element of Morphs V ; :: thesis: verum