let S1, S2 be non empty ManySortedSign ; :: thesis: 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
let A1 be MSAlgebra over S1; :: thesis: 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
let A2 be MSAlgebra over S2; :: thesis: ( A1 is gate`2=den & A2 is gate`2=den implies the Charact of A1 tolerates the Charact of A2 )
assume that
A1: A1 is gate`2=den and
A2: A2 is gate`2=den ; :: thesis: the Charact of A1 tolerates the Charact of A2
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 the Charact of A1) /\ (proj1 the Charact of A2) or the Charact of A1 . x = the Charact of A2 . x )
set C1 = the Charact of A1;
set C2 = the Charact of A2;
assume A3: 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 A2 by XBOOLE_0:def 4;
then x in the carrier' of S2 by PARTFUN1:def 2;
then A4: x = [(x `1),( the Charact of A2 . x)] by A2;
x in dom the Charact of A1 by A3, XBOOLE_0:def 4;
then x in the carrier' of S1 by PARTFUN1:def 2;
then x = [(x `1),( the Charact of A1 . x)] by A1;
hence the Charact of A1 . x = the Charact of A2 . x by A4, XTUPLE_0:1; :: thesis: verum