let U0 be Universal_Algebra; :: thesis: 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)

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

hence
UniAlg_join U0 is associative
by BINOP_1:def 3; :: thesis: verum
let x, y, z be Element of Sub U0; :: thesis: (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; :: thesis: verum

end;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; :: thesis: verum