let A be with_const_op Universal_Algebra; :: thesis: for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 /\ b1) = a2 /\ b2
let a1, b1 be strict non-empty SubAlgebra of A; :: thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 /\ b1) = a2 /\ b2
reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2;
A1: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10;
MSAlg (a1 /\ b1) = MSAlgebra(# (MSSorts (a1 /\ b1)),(MSCharact (a1 /\ b1)) #) by MSUALG_1:def 11;
then A2: the Sorts of (MSAlg (a1 /\ b1)) = 0 .--> the carrier of (a1 /\ b1) by MSUALG_1:def 9;
then dom the Sorts of (MSAlg (a1 /\ b1)) = the carrier of (MSSign A) by A1;
then reconsider D = the Sorts of (MSAlg (a1 /\ b1)) as ManySortedSet of the carrier of (MSSign A) by PARTFUN1:def 2, RELAT_1:def 18;
let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; :: thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies MSAlg (a1 /\ b1) = a2 /\ b2 )
assume A3: ( a2 = MSAlg a1 & b2 = MSAlg b1 ) ; :: thesis: MSAlg (a1 /\ b1) = a2 /\ b2
now :: thesis: for x being object st x in the carrier of (MSSign A) holds
D . x = ( the Sorts of a2 (/\) the Sorts of b2) . x
let x be object ; :: thesis: ( x in the carrier of (MSSign A) implies D . x = ( the Sorts of a2 (/\) the Sorts of b2) . x )
A4: the carrier of a1 meets the carrier of b1 by UNIALG_2:17;
assume A5: x in the carrier of (MSSign A) ; :: thesis: D . x = ( the Sorts of a2 (/\) the Sorts of b2) . x
hence D . x = (0 .--> the carrier of (a1 /\ b1)) . 0 by A2, A1, TARSKI:def 1
.= the carrier of (a1 /\ b1) by FUNCOP_1:72
.= the carrier of a1 /\ the carrier of b1 by A4, UNIALG_2:def 9
.= (0 .--> ( the carrier of a1 /\ the carrier of b1)) . 0 by FUNCOP_1:72
.= ( the Sorts of a2 (/\) the Sorts of b2) . 0 by A3, Th29
.= ( the Sorts of a2 (/\) the Sorts of b2) . x by A1, A5, TARSKI:def 1 ;
:: thesis: verum
end;
then A6: D = the Sorts of a2 (/\) the Sorts of b2 ;
MSSign (a1 /\ b1) = MSSign A by Th7;
then reconsider AA = MSAlg (a1 /\ b1) as strict non-empty MSSubAlgebra of MSAlg A by Th12;
for B being MSSubset of (MSAlg A) st B = the Sorts of AA holds
( B is opers_closed & the Charact of AA = Opers ((MSAlg A),B) ) by MSUALG_2:def 9;
hence MSAlg (a1 /\ b1) = a2 /\ b2 by A6, MSUALG_2:def 16; :: thesis: verum