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;
A3: f,g form_morphism_between S1,S2 by A1;
A4: rng g = the carrier' of S2 by A1, Th24;
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:127
.= rng ( the ResultSort of S2 * g) by A3
.= rng the ResultSort of S2 by A4, A5, RELAT_1:28 ;
thus f .: (InputVertices S1) = (f .: the carrier of S1) \ (f .: (rng the ResultSort of S1)) by A2, FUNCT_1:64
.= InputVertices S2 by A1, A6, Th23 ; :: thesis: f .: (InnerVertices S1) = InnerVertices S2
thus f .: (InnerVertices S1) = InnerVertices S2 by A6; :: thesis: verum