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 Def14;
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 Def15;
A2:
the
carrier of
U2 is
Subset of
U0
by Def7;
A3:
the
carrier of
U3 is
Subset of
U0
by Def7;
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 Def7;
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 Def13
.=
GenUnivAlg B
by A5, Th20
;
(UniAlg_join U0) . (
y,
z)
= U2 "\/" U3
by Def15;
then A7:
(UniAlg_join U0) . (
x,
((UniAlg_join U0) . (y,z)))
= U1 "\/" (U2 "\/" U3)
by Def15;
U1 "\/" (U2 "\/" U3) =
U1 "\/" (GenUnivAlg C)
by Def13
.=
(GenUnivAlg C) "\/" U1
by Th21
.=
GenUnivAlg B
by Th20
;
hence
(UniAlg_join U0) . (
x,
((UniAlg_join U0) . (y,z)))
= (UniAlg_join U0) . (
((UniAlg_join U0) . (x,y)),
z)
by A1, A7, A6, Def15;
verum
end;
hence
UniAlg_join U0 is associative
by BINOP_1:def 3; verum