let S1, S2 be non empty ManySortedSign ; 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; ( 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
; ( 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
; f .: (InnerVertices S1) = InnerVertices S2
thus
f .: (InnerVertices S1) = InnerVertices S2
by A6; verum