let U0 be Universal_Algebra; UniAlg_join U0 is associative
set o = UniAlg_join U0;
for x, y, z being Element of Sub U0 holds (UniAlg_join U0) . x,((UniAlg_join U0) . y,z) = (UniAlg_join U0) . ((UniAlg_join U0) . x,y),z
proof
let x,
y,
z be
Element of
Sub U0;
(UniAlg_join U0) . x,((UniAlg_join U0) . y,z) = (UniAlg_join U0) . ((UniAlg_join U0) . x,y),z
reconsider U1 =
x,
U2 =
y,
U3 =
z as
strict SubAlgebra of
U0 by Def15;
reconsider B = the
carrier of
U1 \/ (the carrier of U2 \/ the carrier of U3) as non
empty set ;
A1:
(UniAlg_join U0) . x,
y = U1 "\/" U2
by Def16;
A2:
the
carrier of
U2 is
Subset of
U0
by Def8;
A3:
the
carrier of
U3 is
Subset of
U0
by Def8;
then reconsider C = the
carrier of
U2 \/ the
carrier of
U3 as non
empty Subset of
U0 by A2, XBOOLE_1:8;
A4:
the
carrier of
U1 is
Subset of
U0
by Def8;
then reconsider D = the
carrier of
U1 \/ the
carrier of
U2 as non
empty Subset of
U0 by A2, XBOOLE_1:8;
the
carrier of
U2 \/ the
carrier of
U3 c= the
carrier of
U0
by A2, A3, XBOOLE_1:8;
then reconsider B =
B as non
empty Subset of
U0 by A4, XBOOLE_1:8;
A5:
B = D \/ the
carrier of
U3
by XBOOLE_1:4;
A6:
(U1 "\/" U2) "\/" U3 =
(GenUnivAlg D) "\/" U3
by Def14
.=
GenUnivAlg B
by A5, Th23
;
(UniAlg_join U0) . y,
z = U2 "\/" U3
by Def16;
then A7:
(UniAlg_join U0) . x,
((UniAlg_join U0) . y,z) = U1 "\/" (U2 "\/" U3)
by Def16;
U1 "\/" (U2 "\/" U3) =
U1 "\/" (GenUnivAlg C)
by Def14
.=
(GenUnivAlg C) "\/" U1
by Th24
.=
GenUnivAlg B
by Th23
;
hence
(UniAlg_join U0) . x,
((UniAlg_join U0) . y,z) = (UniAlg_join U0) . ((UniAlg_join U0) . x,y),
z
by A1, A7, A6, Def16;
verum
end;
hence
UniAlg_join U0 is associative
by BINOP_1:def 3; verum