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 11;
then A3: the Sorts of a2 = 0 .--> the carrier of a1 by MSUALG_1:def 9;
reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2;
A4: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10;
then reconsider W = 0 .--> ( the carrier of a1 \/ the carrier of b1) as ManySortedSet of the carrier of (MSSign A) ;
A5: b2 = MSAlgebra(# (MSSorts b1),(MSCharact b1) #) by A2, MSUALG_1:def 11;
now :: thesis: for x being object st x in the carrier of (MSSign A) holds
W . x = ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x)
let x be object ; :: 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:72
.= ((0 .--> the carrier of a1) . 0) \/ the carrier of b1 by FUNCOP_1:72
.= ((0 .--> the carrier of a1) . 0) \/ ((0 .--> the carrier of b1) . 0) by FUNCOP_1:72
.= ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x) by A3, A5, A7, MSUALG_1:def 9 ;
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 4; :: thesis: verum