let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being MSAlgebra over S1
for A2 being MSAlgebra over S2 st A1 is Boolean & A2 is Boolean holds
the Sorts of A1 tolerates the Sorts of A2
let A1 be MSAlgebra over S1; :: thesis: for A2 being MSAlgebra over S2 st A1 is Boolean & A2 is Boolean holds
the Sorts of A1 tolerates the Sorts of A2
let A2 be MSAlgebra over S2; :: thesis: ( A1 is Boolean & A2 is Boolean implies the Sorts of A1 tolerates the Sorts of A2 )
assume that
A1: A1 is Boolean and
A2: A2 is Boolean ; :: thesis: the Sorts of A1 tolerates the Sorts of A2
A3: the Sorts of A2 = the carrier of S2 --> BOOLEAN by A2, Th57;
the Sorts of A1 = the carrier of S1 --> BOOLEAN by A1, Th57;
hence the Sorts of A1 tolerates the Sorts of A2 by A3, FUNCOP_1:87; :: thesis: verum