let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2 st A1 is gate`2=den & A2 is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 holds
A1 +* A2 is gate`2=den
let A1 be non-empty MSAlgebra of S1; :: thesis: for A2 being non-empty MSAlgebra of S2 st A1 is gate`2=den & A2 is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 holds
A1 +* A2 is gate`2=den
let A2 be non-empty MSAlgebra of S2; :: thesis: ( A1 is gate`2=den & A2 is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 implies A1 +* A2 is gate`2=den )
set A = A1 +* A2;
set S = S1 +* S2;
assume that
A1: ( A1 is gate`2=den & A2 is gate`2=den ) and
A2: the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: A1 +* A2 is gate`2=den
A3: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by A2, Def4;
A4: ( dom the Charact of A1 = the carrier' of S1 & dom the Charact of A2 = the carrier' of S2 ) by PBOOLE:def 3;
A5: the Charact of A1 tolerates the Charact of A2 by A1, Th56;
let g be set ; :: according to CIRCCOMB:def 10 :: thesis: ( g in the carrier' of (S1 +* S2) implies g = [(g `1 ),(the Charact of (A1 +* A2) . g)] )
assume A6: g in the carrier' of (S1 +* S2) ; :: thesis: g = [(g `1 ),(the Charact of (A1 +* A2) . g)]
the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
then ( g in the carrier' of S1 or g in the carrier' of S2 ) by A6, XBOOLE_0:def 3;
then ( ( the Charact of (A1 +* A2) . g = the Charact of A1 . g & [(g `1 ),(the Charact of A1 . g)] = g ) or ( the Charact of (A1 +* A2) . g = the Charact of A2 . g & [(g `1 ),(the Charact of A2 . g)] = g ) ) by A1, A3, A4, A5, Def10, FUNCT_4:14, FUNCT_4:16;
hence g = [(g `1 ),(the Charact of (A1 +* A2) . g)] ; :: thesis: verum