theorem Th28: :: CIRCTRM1:28

for S1, S2 being 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 )