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
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 A1: ( a2 = MSAlg a1 & b2 = MSAlg b1 ) ; :: thesis: MSAlg (a1 /\ b1) = a2 /\ b2
A2: MSSign (a1 /\ b1) = MSSign A by Th7;
MSAlg (a1 /\ b1) = MSAlgebra(# (MSSorts (a1 /\ b1)),(MSCharact (a1 /\ b1)) #) by MSUALG_1:def 16;
then A3: the Sorts of (MSAlg (a1 /\ b1)) = 0 .--> the carrier of (a1 /\ b1) 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;
then dom the Sorts of (MSAlg (a1 /\ b1)) = the carrier of (MSSign A) by A3, FUNCOP_1:19;
then reconsider D = the Sorts of (MSAlg (a1 /\ b1)) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A5: D = the Sorts of a2 /\ the Sorts of b2

proof

now

let x be set ; :: thesis: ( x in the carrier of (MSSign A) implies D . x = (the Sorts of a2 /\ the Sorts of b2) . x )
assume A6: x in the carrier of (MSSign A) ; :: thesis: D . x = (the Sorts of a2 /\ the Sorts of b2) . x
A7: the carrier of a1 meets the carrier of b1 by UNIALG_2:20;
thus D . x = (0 .--> the carrier of (a1 /\ b1)) . 0 by A3, A4, A6, TARSKI:def 1
.= the carrier of (a1 /\ b1) by FUNCOP_1:87
.= the carrier of a1 /\ the carrier of b1 by A7, UNIALG_2:def 10
.= (0 .--> (the carrier of a1 /\ the carrier of b1)) . 0 by FUNCOP_1:87
.= (the Sorts of a2 /\ the Sorts of b2) . 0 by A1, Th29
.= (the Sorts of a2 /\ the Sorts of b2) . x by A4, A6, TARSKI:def 1 ; :: thesis: verum

end;

hence D = the Sorts of a2 /\ the Sorts of b2 by PBOOLE:3; :: thesis: verum

end;

reconsider AA = MSAlg (a1 /\ b1) as strict non-empty MSSubAlgebra of MSAlg A by A2, 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 10;
hence MSAlg (a1 /\ b1) = a2 /\ b2 by A5, MSUALG_2:def 17; :: thesis: verum