let G1, G2 be non empty non void Circuit-like ManySortedSign ; for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
let f, g be Function; for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
let C1 be non-empty Circuit of G1; for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
let C2 be non-empty Circuit of G2; ( C1,C2 are_similar_wrt f,g implies ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) )
assume
C1,C2 are_similar_wrt f,g
; ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
then
G1,G2 are_equivalent_wrt f,g
by Th36;
hence
( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
by Th28; verum