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: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def 2;
let x be Vertex of (S1 +* S2); :: according to CIRCCOMB:def 14 :: thesis: the Sorts of (A1 +* A2) . x = BOOLEAN
A2: dom the Sorts of A2 = the carrier of S2 by PARTFUN1:def 2;
the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
then A3: ( x in the carrier of S1 or x in the carrier of S2 ) by XBOOLE_0:def 3;
A4: the Sorts of A2 = the carrier of S2 --> BOOLEAN by Th65;
A5: the Sorts of A1 = the carrier of S1 --> BOOLEAN by Th65;
then A6: the Sorts of A1 tolerates the Sorts of A2 by A4, FUNCOP_1:87;
then the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by Def4;
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 A5, A4, A6, A1, A2, A3, FUNCOP_1:7, FUNCT_4:13, FUNCT_4:15;
hence the Sorts of (A1 +* A2) . x = BOOLEAN ; :: thesis: verum