let S1, S2 be non empty ManySortedSign ; :: thesis: for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 )
let f, g be Function; :: thesis: ( S1,S2 are_equivalent_wrt f,g implies ( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 ) )
assume A1: S1,S2 are_equivalent_wrt f,g ; :: thesis: ( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 )
A2: f is one-to-one by A1, Def9;
A3: f,g form_morphism_between S1,S2 by A1, Def9;
A4: rng g = the carrier' of S2 by A1, Th25;
A5: dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def 1;
A6: f .: (rng the ResultSort of S1) = rng (f * the ResultSort of S1) by RELAT_1:160
.= rng ( the ResultSort of S2 * g) by A3, PUA2MSS1:def 13
.= rng the ResultSort of S2 by A4, A5, RELAT_1:47 ;
thus f .: (InputVertices S1) = (f .: the carrier of S1) \ (f .: (rng the ResultSort of S1)) by A2, FUNCT_1:123
.= InputVertices S2 by A1, A6, Th24 ; :: thesis: f .: (InnerVertices S1) = InnerVertices S2
thus f .: (InnerVertices S1) = InnerVertices S2 by A6; :: thesis: verum