let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is associative
let U0 be non-empty MSAlgebra over S; :: thesis:
set o = MSAlg_join U0;
for x, y, z being Element of MSSub U0 holds () . (x,(() . (y,z))) = () . ((() . (x,y)),z)
proof
let x, y, z be Element of MSSub U0; :: thesis: () . (x,(() . (y,z))) = () . ((() . (x,y)),z)
reconsider U1 = x, U2 = y, U3 = z as strict MSSubAlgebra of U0 by Def19;
set B = the Sorts of U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3);
A1: (MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20;
the Sorts of U2 is MSSubset of U0 by Def9;
then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def 18;
the Sorts of U3 is MSSubset of U0 by Def9;
then the Sorts of U3 c= the Sorts of U0 by PBOOLE:def 18;
then A3: the Sorts of U2 (\/) the Sorts of U3 c= the Sorts of U0 by ;
then reconsider C = the Sorts of U2 (\/) the Sorts of U3 as MSSubset of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by Def9;
then A4: the Sorts of U1 c= the Sorts of U0 by PBOOLE:def 18;
then A5: the Sorts of U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3) c= the Sorts of U0 by ;
the Sorts of U1 (\/) the Sorts of U2 c= the Sorts of U0 by ;
then reconsider D = the Sorts of U1 (\/) the Sorts of U2 as MSSubset of U0 by PBOOLE:def 18;
reconsider B = the Sorts of U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3) as MSSubset of U0 by ;
A6: B = D (\/) the Sorts of U3 by PBOOLE:28;
A7: (U1 "\/" U2) "\/" U3 = () "\/" U3 by Def18
.= GenMSAlg B by ;
(MSAlg_join U0) . (y,z) = U2 "\/" U3 by Def20;
then A8: (MSAlg_join U0) . (x,(() . (y,z))) = U1 "\/" (U2 "\/" U3) by Def20;
U1 "\/" (U2 "\/" U3) = U1 "\/" () by Def18
.= () "\/" U1 by Th26
.= GenMSAlg B by Th24 ;
hence (MSAlg_join U0) . (x,(() . (y,z))) = () . ((() . (x,y)),z) by A1, A8, A7, Def20; :: thesis: verum
end;
hence MSAlg_join U0 is associative by BINOP_1:def 3; :: thesis: verum