for S1, S2 being non empty ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
f .: (InnerVertices S1) c= InnerVertices S2