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 V2() 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 #
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
; ( 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 )
; verum