let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is associative

let U0 be non-empty MSAlgebra over S; :: thesis: 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)

let U0 be non-empty MSAlgebra over S; :: thesis: 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

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

set B = the Sorts of U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3);

A1: (MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20;

the Sorts of U2 is MSSubset of U0 by Def9;

then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def 18;

the Sorts of U3 is MSSubset of U0 by Def9;

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 Def9;

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 Def18

.= GenMSAlg B by A6, Th24 ;

(MSAlg_join U0) . (y,z) = U2 "\/" U3 by Def20;

then A8: (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = U1 "\/" (U2 "\/" U3) by Def20;

U1 "\/" (U2 "\/" U3) = U1 "\/" (GenMSAlg C) by Def18

.= (GenMSAlg C) "\/" U1 by Th26

.= GenMSAlg B by Th24 ;

hence (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z) by A1, A8, A7, Def20; :: thesis: verum

end;reconsider U1 = x, U2 = y, U3 = z as strict MSSubAlgebra of U0 by Def19;

set B = the Sorts of U1 (\/) ( the Sorts of U2 (\/) the Sorts of U3);

A1: (MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20;

the Sorts of U2 is MSSubset of U0 by Def9;

then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def 18;

the Sorts of U3 is MSSubset of U0 by Def9;

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 Def9;

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 Def18

.= GenMSAlg B by A6, Th24 ;

(MSAlg_join U0) . (y,z) = U2 "\/" U3 by Def20;

then A8: (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = U1 "\/" (U2 "\/" U3) by Def20;

U1 "\/" (U2 "\/" U3) = U1 "\/" (GenMSAlg C) by Def18

.= (GenMSAlg C) "\/" U1 by Th26

.= GenMSAlg B by Th24 ;

hence (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z) by A1, A8, A7, Def20; :: thesis: verum