let G1, G2 be non empty non void Circuit-like ManySortedSign ; :: thesis: 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
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
let f, g be Function; :: thesis: 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
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
let C1 be non-empty Circuit of G1; :: thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
let C2 be non-empty Circuit of G2; :: thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable ) )
assume A1: C1,C2 are_similar_wrt f,g ; :: thesis: for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
then A2: C2,C1 are_similar_wrt f " ,g " by Th40;
let s1 be State of C1; :: thesis: for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
let s2 be State of C2; :: thesis: ( s1 = s2 * f implies ( s1 is stable iff s2 is stable ) )
assume A3: s1 = s2 * f ; :: thesis: ( s1 is stable iff s2 is stable )
A4: s2 = s1 * (f " ) by A1, A3, Th52;
thus ( s1 is stable implies s2 is stable ) :: thesis: ( s2 is stable implies s1 is stable )

proof

assume s1 = Following s1 ; :: according to CIRCUIT2:def 6 :: thesis: s2 is stable
hence s2 = Following s2 by A2, A4, Th55; :: according to CIRCUIT2:def 6 :: thesis: verum

end;

assume s2 = Following s2 ; :: according to CIRCUIT2:def 6 :: thesis: s1 is stable
hence s1 = Following s1 by A1, A3, Th55; :: according to CIRCUIT2:def 6 :: thesis: verum