let U0 be Universal_Algebra; :: thesis:
set o = UniAlg_join U0;
for x, y, z being Element of Sub U0 holds () . (x,(() . (y,z))) = () . ((() . (x,y)),z)
proof
let x, y, z be Element of Sub U0; :: thesis: () . (x,(() . (y,z))) = () . ((() . (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 ;
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 ;
the carrier of U2 \/ the carrier of U3 c= the carrier of U0 by ;
then reconsider B = B as non empty Subset of U0 by ;
A5: B = D \/ the carrier of U3 by XBOOLE_1:4;
A6: (U1 "\/" U2) "\/" U3 = () "\/" U3 by Def13
.= GenUnivAlg B by ;
(UniAlg_join U0) . (y,z) = U2 "\/" U3 by Def15;
then A7: (UniAlg_join U0) . (x,(() . (y,z))) = U1 "\/" (U2 "\/" U3) by Def15;
U1 "\/" (U2 "\/" U3) = U1 "\/" () by Def13
.= () "\/" U1 by Th21
.= GenUnivAlg B by Th20 ;
hence (UniAlg_join U0) . (x,(() . (y,z))) = () . ((() . (x,y)),z) by A1, A7, A6, Def15; :: thesis: verum
end;
hence UniAlg_join U0 is associative by BINOP_1:def 3; :: thesis: verum