set CHARACT = the Charact of A1 +* the Charact of A2;
set SA1 = the Sorts of A1;
set SA2 = the Sorts of A2;
set S = S1 +* S2;
set I = the carrier of (S1 +* S2);
set I1 = the carrier of S1;
set I2 = the carrier of S2;
set SA12 = ( the Sorts of A1 #) +* ( the Sorts of A2 #);
A2: dom ( the Sorts of A2 #) = the carrier of S2 * by PARTFUN1:def 2;
A3: the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
A4: rng the ResultSort of S2 c= the carrier of S2 by RELAT_1:def 19;
A5: 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 reconsider SORTS = the Sorts of A1 +* the Sorts of A2 as non-empty ManySortedSet of the carrier of (S1 +* S2) ;
A6: dom (SORTS #) = the carrier of (S1 +* S2) * by PARTFUN1:def 2;
A7: SORTS = the Sorts of A1 \/ the Sorts of A2 by A1, FUNCT_4:30;
then A8: the Sorts of A2 # c= SORTS # by Th1, XBOOLE_1:7;
A9: dom (( the Sorts of A1 #) +* ( the Sorts of A2 #)) = ( the carrier of S1 *) \/ ( the carrier of S2 *) by PARTFUN1:def 2;
A10: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def 2;
rng the ResultSort of S1 c= the carrier of S1 by RELAT_1:def 19;
then A11: ( the Sorts of A1 +* the Sorts of A2) * ( the ResultSort of S1 +* the ResultSort of S2) = ( the Sorts of A1 * the ResultSort of S1) +* ( the Sorts of A2 * the ResultSort of S2) by A1, A10, A5, A4, FUNCT_4:69;
A12: rng the Arity of S2 c= the carrier of S2 * by RELAT_1:def 19;
A13: dom ( the Sorts of A1 #) = the carrier of S1 * by PARTFUN1:def 2;
A14: the Sorts of A1 # tolerates the Sorts of A2 #

proof

let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 ( the Sorts of A1 #)) /\ (proj1 ( the Sorts of A2 #)) or ( the Sorts of A1 #) . x = ( the Sorts of A2 #) . x )
assume A15: x in (dom ( the Sorts of A1 #)) /\ (dom ( the Sorts of A2 #)) ; :: thesis: ( the Sorts of A1 #) . x = ( the Sorts of A2 #) . x
then reconsider i1 = x as Element of the carrier of S1 * by A13, XBOOLE_0:def 4;
reconsider i2 = x as Element of the carrier of S2 * by A2, A15, XBOOLE_0:def 4;
A16: rng i1 c= the carrier of S1 by FINSEQ_1:def 4;
A17: rng i2 c= the carrier of S2 by FINSEQ_1:def 4;
thus ( the Sorts of A1 #) . x = product ( the Sorts of A1 * i1) by FINSEQ_2:def 5
.= product ( the Sorts of A2 * i2) by A1, A10, A5, A16, A17, PARTFUN1:79
.= ( the Sorts of A2 #) . x by FINSEQ_2:def 5 ; :: thesis: verum

end;

then A18: ( the Sorts of A1 #) +* ( the Sorts of A2 #) = ( the Sorts of A1 #) \/ ( the Sorts of A2 #) by FUNCT_4:30;
the Sorts of A1 # c= SORTS # by A7, Th1, XBOOLE_1:7;
then A19: ( the Sorts of A1 #) +* ( the Sorts of A2 #) c= SORTS # by A18, A8, XBOOLE_1:8;
A20: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
A21: rng the Arity of (S1 +* S2) c= the carrier of (S1 +* S2) * by RELAT_1:def 19;
A22: rng the Arity of S1 c= the carrier of S1 * by RELAT_1:def 19;
then A23: (rng the Arity of S1) \/ (rng the Arity of S2) c= ( the carrier of S1 *) \/ ( the carrier of S2 *) by A12, XBOOLE_1:13;
A24: the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
then rng the Arity of (S1 +* S2) c= (rng the Arity of S1) \/ (rng the Arity of S2) by FUNCT_4:17;
then A25: rng the Arity of (S1 +* S2) c= dom (( the Sorts of A1 #) +* ( the Sorts of A2 #)) by A23, A9;
A26: ( the Sorts of A1 #) +* ( the Sorts of A2 #) tolerates SORTS # by A19, PARTFUN1:54;
A27: (( the Sorts of A1 #) +* ( the Sorts of A2 #)) * ( the Arity of S1 +* the Arity of S2) = (( the Sorts of A1 #) * the Arity of S1) +* (( the Sorts of A2 #) * the Arity of S2) by A13, A2, A22, A12, A14, FUNCT_4:69;
reconsider CHARACT = the Charact of A1 +* the Charact of A2 as ManySortedFunction of (SORTS #) * the Arity of (S1 +* S2),SORTS * the ResultSort of (S1 +* S2) by A20, A24, A3, A6, A21, A25, A11, A26, A27, PARTFUN1:79;
reconsider A = MSAlgebra(# SORTS,CHARACT #) as strict non-empty MSAlgebra over S1 +* S2 by MSUALG_1:def 3;
take A ; :: thesis: ( the Sorts of A = the Sorts of A1 +* the Sorts of A2 & the Charact of A = the Charact of A1 +* the Charact of A2 )
thus ( the Sorts of A = the Sorts of A1 +* the Sorts of A2 & the Charact of A = the Charact of A1 +* the Charact of A2 ) ; :: thesis: verum