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 4;
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 4;
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 4;
A7: SORTS = the Sorts of A1 \/ the Sorts of A2 by A1, FUNCT_4:31;
then A8: the Sorts of A2 # c= SORTS # by Th3, XBOOLE_1:7;
A9: dom ((the Sorts of A1 # ) +* (the Sorts of A2 # )) = (the carrier of S1 * ) \/ (the carrier of S2 * ) by PARTFUN1:def 4;
A10: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def 4;
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:73;
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 4;
A14: the Sorts of A1 # tolerates the Sorts of A2 #

proof

let x be set ; :: according to PARTFUN1:def 6 :: 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 PBOOLE:def 19
.= product (the Sorts of A2 * i2) by A1, A10, A5, A16, A17, Th2
.= (the Sorts of A2 # ) . x by PBOOLE:def 19 ; :: thesis: verum

end;

then A18: (the Sorts of A1 # ) +* (the Sorts of A2 # ) = (the Sorts of A1 # ) \/ (the Sorts of A2 # ) by FUNCT_4:31;
the Sorts of A1 # c= SORTS # by A7, Th3, 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:18;
then A25: rng the Arity of (S1 +* S2) c= dom ((the Sorts of A1 # ) +* (the Sorts of A2 # )) by A23, A9, XBOOLE_1:1;
((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:73;
then 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, A19, A25, A11, Th2, PARTFUN1:135;
reconsider A = MSAlgebra(# SORTS,CHARACT #) as strict non-empty MSAlgebra of S1 +* S2 by MSUALG_1:def 8;
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