let A be Universal_Algebra; :: thesis: for a1, b1 being strict SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 \/ the Sorts of b2 = 0 .--> (the carrier of a1 \/ the carrier of b1)
let a1, b1 be strict SubAlgebra of A; :: thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 \/ the Sorts of b2 = 0 .--> (the carrier of a1 \/ the carrier of b1)
let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; :: thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies the Sorts of a2 \/ the Sorts of b2 = 0 .--> (the carrier of a1 \/ the carrier of b1) )
assume that
A1: a2 = MSAlg a1 and
A2: b2 = MSAlg b1 ; :: thesis: the Sorts of a2 \/ the Sorts of b2 = 0 .--> (the carrier of a1 \/ the carrier of b1)
a2 = MSAlgebra(# (MSSorts a1),(MSCharact a1) #) by A1, MSUALG_1:def 16;
then A3: the Sorts of a2 = 0 .--> the carrier of a1 by MSUALG_1:def 14;
reconsider ff1 = (*--> 0 ) * (signature A) as Function of (dom (signature A)),({0 } * ) by MSUALG_1:7;
A4: MSSign A = ManySortedSign(# {0 },(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:16;
dom (0 .--> (the carrier of a1 \/ the carrier of b1)) = {0 } by FUNCOP_1:19;
then reconsider W = 0 .--> (the carrier of a1 \/ the carrier of b1) as ManySortedSet of the carrier of (MSSign A) by A4, PARTFUN1:def 4;
A5: b2 = MSAlgebra(# (MSSorts b1),(MSCharact b1) #) by A2, MSUALG_1:def 16;

now

let x be set ; :: thesis: ( x in the carrier of (MSSign A) implies W . x = (the Sorts of a2 . x) \/ (the Sorts of b2 . x) )
assume A6: x in the carrier of (MSSign A) ; :: thesis: W . x = (the Sorts of a2 . x) \/ (the Sorts of b2 . x)
then A7: x = 0 by A4, TARSKI:def 1;
W . x = (0 .--> (the carrier of a1 \/ the carrier of b1)) . 0 by A4, A6, TARSKI:def 1
.= the carrier of a1 \/ the carrier of b1 by FUNCOP_1:87
.= ((0 .--> the carrier of a1) . 0 ) \/ the carrier of b1 by FUNCOP_1:87
.= ((0 .--> the carrier of a1) . 0 ) \/ ((0 .--> the carrier of b1) . 0 ) by FUNCOP_1:87
.= (the Sorts of a2 . x) \/ (the Sorts of b2 . x) by A3, A5, A7, MSUALG_1:def 14 ;
hence W . x = (the Sorts of a2 . x) \/ (the Sorts of b2 . x) ; :: thesis: verum

end;

hence the Sorts of a2 \/ the Sorts of b2 = 0 .--> (the carrier of a1 \/ the carrier of b1) by PBOOLE:def 7; :: thesis: verum