let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being Boolean MSAlgebra of S1
for A2 being Boolean MSAlgebra of S2 holds A1 +* A2 is Boolean
let A1 be Boolean MSAlgebra of S1; :: thesis: for A2 being Boolean MSAlgebra of S2 holds A1 +* A2 is Boolean
let A2 be Boolean MSAlgebra of S2; :: thesis: A1 +* A2 is Boolean
set A = A1 +* A2;
set S = S1 +* S2;
A1: ( the Sorts of A1 = the carrier of S1 --> BOOLEAN & the Sorts of A2 = the carrier of S2 --> BOOLEAN ) by Th65;
then A2: the Sorts of A1 tolerates the Sorts of A2 by Th4;
then A3: the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by Def4;
A4: ( dom the Sorts of A1 = the carrier of S1 & dom the Sorts of A2 = the carrier of S2 ) by PARTFUN1:def 4;
let x be Vertex of (S1 +* S2); :: according to CIRCCOMB:def 15 :: thesis: the Sorts of (A1 +* A2) . x = BOOLEAN
the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
then ( x in the carrier of S1 or x in the carrier of S2 ) by XBOOLE_0:def 3;
then ( ( the Sorts of (A1 +* A2) . x = the Sorts of A1 . x & the Sorts of A1 . x = BOOLEAN ) or ( the Sorts of (A1 +* A2) . x = the Sorts of A2 . x & the Sorts of A2 . x = BOOLEAN ) ) by A1, A2, A3, A4, FUNCOP_1:13, FUNCT_4:14, FUNCT_4:16;
hence the Sorts of (A1 +* A2) . x = BOOLEAN ; :: thesis: verum