let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over 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 over S1; :: thesis: for A2 being non-empty MSAlgebra over 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 over 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 and
A2: A2 is gate`2=den and
A3: the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: A1 +* A2 is gate`2=den
A4: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by A3, Def4;
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)] )
A5: dom the Charact of A1 = the carrier' of S1 by PARTFUN1:def 2;
A6: dom the Charact of A2 = the carrier' of S2 by PARTFUN1:def 2;
A7: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
assume g in the carrier' of (S1 +* S2) ; :: thesis: g = [(g `1),( the Charact of (A1 +* A2) . g)]
then A8: ( g in the carrier' of S1 or g in the carrier' of S2 ) by A7, XBOOLE_0:def 3;
the Charact of A1 tolerates the Charact of A2 by A1, A2, Th48;
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, A2, A4, A5, A6, A8, FUNCT_4:13, FUNCT_4:15;
hence g = [(g `1),( the Charact of (A1 +* A2) . g)] ; :: thesis: verum