set S = S1 +* S2;
A2: ( the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 & the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 & the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 & the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 ) by Def2;
reconsider SORTS = the Sorts of A1 +* the Sorts of A2 as V2() ManySortedSet of by A2;
set SA1 = the Sorts of A1;
set SA2 = the Sorts of A2;
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 # );
set CHARACT = the Charact of A1 +* the Charact of A2;
A3: ( dom (the Sorts of A1 # ) = the carrier of S1 * & dom (the Sorts of A2 # ) = the carrier of S2 * & dom the Sorts of A1 = the carrier of S1 & dom the Sorts of A2 = the carrier of S2 & dom (SORTS # ) = the carrier of (S1 +* S2) * & dom SORTS = the carrier of (S1 +* S2) ) by PARTFUN1:def 4;
A4: ( rng the Arity of S1 c= the carrier of S1 * & rng the Arity of S2 c= the carrier of S2 * & rng the Arity of (S1 +* S2) c= the carrier of (S1 +* S2) * & rng the ResultSort of S1 c= the carrier of S1 & rng the ResultSort of S2 c= the carrier of S2 ) by RELAT_1:def 19;
then A5: (rng the Arity of S1) \/ (rng the Arity of S2) c= (the carrier of S1 * ) \/ (the carrier of S2 * ) by XBOOLE_1:13;
SORTS = the Sorts of A1 \/ the Sorts of A2 by A1, FUNCT_4:31;
then A6: ( the Sorts of A1 c= SORTS & the Sorts of A2 c= SORTS ) by XBOOLE_1:7;
A7: the Sorts of A1 # tolerates the Sorts of A2 #

proof

let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (dom (the Sorts of A1 # )) /\ (dom (the Sorts of A2 # )) or (the Sorts of A1 # ) . x = (the Sorts of A2 # ) . x )
assume A8: 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 A3, XBOOLE_0:def 4;
reconsider i2 = x as Element of the carrier of S2 * by A3, A8, XBOOLE_0:def 4;
A9: ( rng i1 c= the carrier of S1 & 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, A3, A9, Th2
.= (the Sorts of A2 # ) . x by PBOOLE:def 19 ; :: thesis: verum

end;

then ( (the Sorts of A1 # ) +* (the Sorts of A2 # ) = (the Sorts of A1 # ) \/ (the Sorts of A2 # ) & the Sorts of A1 # c= SORTS # & the Sorts of A2 # c= SORTS # ) by A6, Th3, FUNCT_4:31;
then A10: (the Sorts of A1 # ) +* (the Sorts of A2 # ) c= SORTS # by XBOOLE_1:8;
( rng the Arity of (S1 +* S2) c= (rng the Arity of S1) \/ (rng the Arity of S2) & dom ((the Sorts of A1 # ) +* (the Sorts of A2 # )) = (the carrier of S1 * ) \/ (the carrier of S2 * ) ) by A2, FUNCT_4:18, PARTFUN1:def 4;
then A11: rng the Arity of (S1 +* S2) c= dom ((the Sorts of A1 # ) +* (the Sorts of A2 # )) by A5, 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) & (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, A3, A4, A7, 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 A2, A3, A4, A10, 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