let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being MSAlgebra of S1
for A2 being MSAlgebra of S2 st A1 is gate`2=den & A2 is gate`2=den holds
the Charact of A1 tolerates the Charact of A2
let A1 be MSAlgebra of S1; :: thesis: for A2 being MSAlgebra of S2 st A1 is gate`2=den & A2 is gate`2=den holds
the Charact of A1 tolerates the Charact of A2
let A2 be MSAlgebra of S2; :: thesis: ( A1 is gate`2=den & A2 is gate`2=den implies the Charact of A1 tolerates the Charact of A2 )
assume A1: ( A1 is gate`2=den & A2 is gate`2=den ) ; :: thesis: the Charact of A1 tolerates the Charact of A2
set C1 = the Charact of A1;
set C2 = the Charact of A2;
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (dom the Charact of A1) /\ (dom the Charact of A2) or the Charact of A1 . x = the Charact of A2 . x )
assume x in (dom the Charact of A1) /\ (dom the Charact of A2) ; :: thesis: the Charact of A1 . x = the Charact of A2 . x
then ( x in dom the Charact of A1 & x in dom the Charact of A2 ) by XBOOLE_0:def 4;
then ( x in the carrier' of S1 & x in the carrier' of S2 ) by PARTFUN1:def 4;
then ( x = [(x `1 ),(the Charact of A1 . x)] & x = [(x `1 ),(the Charact of A2 . x)] ) by A1, Def10;
hence the Charact of A1 . x = the Charact of A2 . x by ZFMISC_1:33; :: thesis: verum