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 by PUA2MSS1:def 13;
then f .: (InnerVertices S1) = rng (the ResultSort of S2 * g) by RELAT_1:160;
hence f .: (InnerVertices S1) c= InnerVertices S2 by RELAT_1:45; :: thesis: verum