for S1, S2 being non empty ManySortedSign
for A1 being MSAlgebra over S1
for A2 being MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den holds
the Charact of A1 tolerates the Charact of A2