set RESULT = the ResultSort of S1 +* the ResultSort of S2;
set ARITY = the Arity of S1 +* the Arity of S2;
set OPER = the carrier' of S1 \/ the carrier' of S2;
reconsider CARR = the carrier of S1 \/ the carrier of S2 as non empty set ;
A1:
dom the ResultSort of S2 = the carrier' of S2
by FUNCT_2:def 1;
dom the ResultSort of S1 = the carrier' of S1
by FUNCT_2:def 1;
then A2:
dom ( the ResultSort of S1 +* the ResultSort of S2) = the carrier' of S1 \/ the carrier' of S2
by A1, FUNCT_4:def 1;
A3:
the carrier of S1 c= CARR
by XBOOLE_1:7;
A4:
the carrier of S2 c= CARR
by XBOOLE_1:7;
rng the ResultSort of S2 c= the carrier of S2
by RELAT_1:def 19;
then A5:
rng the ResultSort of S2 c= CARR
by A4;
rng the ResultSort of S1 c= the carrier of S1
by RELAT_1:def 19;
then
rng the ResultSort of S1 c= CARR
by A3;
then A6:
(rng the ResultSort of S1) \/ (rng the ResultSort of S2) c= CARR
by A5, XBOOLE_1:8;
rng ( the ResultSort of S1 +* the ResultSort of S2) c= (rng the ResultSort of S1) \/ (rng the ResultSort of S2)
by FUNCT_4:17;
then
rng ( the ResultSort of S1 +* the ResultSort of S2) c= CARR
by A6;
then reconsider RESULT = the ResultSort of S1 +* the ResultSort of S2 as Function of ( the carrier' of S1 \/ the carrier' of S2),CARR by A2, FUNCT_2:def 1, RELSET_1:4;
A7:
dom the Arity of S2 = the carrier' of S2
by FUNCT_2:def 1;
dom the Arity of S1 = the carrier' of S1
by FUNCT_2:def 1;
then A8:
dom ( the Arity of S1 +* the Arity of S2) = the carrier' of S1 \/ the carrier' of S2
by A7, FUNCT_4:def 1;
A9:
rng the Arity of S1 c= the carrier of S1 *
by RELAT_1:def 19;
A10:
rng the Arity of S2 c= the carrier of S2 *
by RELAT_1:def 19;
the carrier of S2 * c= CARR *
by FINSEQ_1:62, XBOOLE_1:7;
then A11:
rng the Arity of S2 c= CARR *
by A10;
the carrier of S1 * c= CARR *
by FINSEQ_1:62, XBOOLE_1:7;
then
rng the Arity of S1 c= CARR *
by A9;
then A12:
(rng the Arity of S1) \/ (rng the Arity of S2) c= CARR *
by A11, XBOOLE_1:8;
rng ( the Arity of S1 +* the Arity of S2) c= (rng the Arity of S1) \/ (rng the Arity of S2)
by FUNCT_4:17;
then
rng ( the Arity of S1 +* the Arity of S2) c= CARR *
by A12;
then reconsider ARITY = the Arity of S1 +* the Arity of S2 as Function of ( the carrier' of S1 \/ the carrier' of S2),(CARR *) by A8, FUNCT_2:def 1, RELSET_1:4;
take
ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #)
; ( the carrier of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the carrier of S1 \/ the carrier of S2 & the carrier' of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the carrier' of S1 \/ the carrier' of S2 & the Arity of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the Arity of S1 +* the Arity of S2 & the ResultSort of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the ResultSort of S1 +* the ResultSort of S2 )
thus
( the carrier of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the carrier of S1 \/ the carrier of S2 & the carrier' of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the carrier' of S1 \/ the carrier' of S2 & the Arity of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the Arity of S1 +* the Arity of S2 & the ResultSort of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the ResultSort of S1 +* the ResultSort of S2 )
; verum