let A be set ; :: thesis: for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) = (K ^ L) ^ M
let K, L, M be Element of Normal_forms_on A; :: thesis: K ^ (L ^ M) = (K ^ L) ^ M
A1: ( L ^ M = M ^ L & K ^ L = L ^ K ) by Th48;

A2: now :: thesis: for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) c= (K ^ L) ^ M

let K, L, M be Element of Normal_forms_on A; :: thesis: K ^ (L ^ M) c= (K ^ L) ^ M

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in K ^ (L ^ M) holds
a in (K ^ L) ^ M

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in K ^ (L ^ M) implies a in (K ^ L) ^ M )
assume a in K ^ (L ^ M) ; :: thesis: a in (K ^ L) ^ M
then consider b, c being Element of DISJOINT_PAIRS A such that
A3: b in K and
A4: c in L ^ M and
A5: a = b \/ c by Th34;
consider b1, c1 being Element of DISJOINT_PAIRS A such that
A6: b1 in L and
A7: c1 in M and
A8: c = b1 \/ c1 by A4, Th34;
reconsider d = b \/ (b1 \/ c1) as Element of DISJOINT_PAIRS A by A5, A8;
A9: b \/ (b1 \/ c1) = (b \/ b1) \/ c1 by Th3;
then b \/ b1 c= d by Th10;
then reconsider c2 = b \/ b1 as Element of DISJOINT_PAIRS A by Th26;
c2 in K ^ L by A3, A6, Th35;
hence a in (K ^ L) ^ M by A5, A7, A8, A9, Th35; :: thesis: verum

end;

hence K ^ (L ^ M) c= (K ^ L) ^ M by Lm5; :: thesis: verum

end;

then A10: K ^ (L ^ M) c= (K ^ L) ^ M ;
( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th48;
then (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2;
hence K ^ (L ^ M) = (K ^ L) ^ M by A10; :: thesis: verum