let S be non empty non void ManySortedSign ; for U0 being non-empty MSAlgebra of S holds MSAlg_join U0 is associative
let U0 be non-empty MSAlgebra of S; MSAlg_join U0 is associative
set o = MSAlg_join U0;
for x, y, z being Element of MSSub U0 holds (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z)
proof
let x,
y,
z be
Element of
MSSub U0;
(MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z)
reconsider U1 =
x,
U2 =
y,
U3 =
z as
strict MSSubAlgebra of
U0 by Def20;
set B = the
Sorts of
U1 \/ ( the Sorts of U2 \/ the Sorts of U3);
A1:
(MSAlg_join U0) . (
x,
y)
= U1 "\/" U2
by Def21;
the
Sorts of
U2 is
MSSubset of
U0
by Def10;
then A2:
the
Sorts of
U2 c= the
Sorts of
U0
by PBOOLE:def 18;
the
Sorts of
U3 is
MSSubset of
U0
by Def10;
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 A2, PBOOLE:16;
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 Def10;
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 A3, PBOOLE:16;
the
Sorts of
U1 \/ the
Sorts of
U2 c= the
Sorts of
U0
by A4, A2, PBOOLE:16;
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 A5, PBOOLE:def 18;
A6:
B = D \/ the
Sorts of
U3
by PBOOLE:28;
A7:
(U1 "\/" U2) "\/" U3 =
(GenMSAlg D) "\/" U3
by Def19
.=
GenMSAlg B
by A6, Th25
;
(MSAlg_join U0) . (
y,
z)
= U2 "\/" U3
by Def21;
then A8:
(MSAlg_join U0) . (
x,
((MSAlg_join U0) . (y,z)))
= U1 "\/" (U2 "\/" U3)
by Def21;
U1 "\/" (U2 "\/" U3) =
U1 "\/" (GenMSAlg C)
by Def19
.=
(GenMSAlg C) "\/" U1
by Th27
.=
GenMSAlg B
by Th25
;
hence
(MSAlg_join U0) . (
x,
((MSAlg_join U0) . (y,z)))
= (MSAlg_join U0) . (
((MSAlg_join U0) . (x,y)),
z)
by A1, A8, A7, Def21;
verum
end;
hence
MSAlg_join U0 is associative
by BINOP_1:def 3; verum