let S1, S2 be non empty ManySortedSign ; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
f .: (InnerVertices S1) c= InnerVertices S2
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies f .: (InnerVertices S1) c= InnerVertices S2 )
assume f,g form_morphism_between S1,S2 ; :: thesis: f .: (InnerVertices S1) c= InnerVertices S2
then f * the ResultSort of S1 = the ResultSort of S2 * g ;
then f .: (InnerVertices S1) = rng ( the ResultSort of S2 * g) by RELAT_1:127;
hence f .: (InnerVertices S1) c= InnerVertices S2 by RELAT_1:26; :: thesis: verum