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