let A be set ; :: thesis: for K, L, M being Element of Normal_forms_on A holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
let K, L, M be Element of Normal_forms_on A; :: thesis: K ^ (L \/ M) = (K ^ L) \/ (K ^ M)

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

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in K ^ (L \/ M) implies a in (K ^ L) \/ (K ^ M) )
assume a in K ^ (L \/ M) ; :: thesis: a in (K ^ L) \/ (K ^ M)
then consider b, c being Element of DISJOINT_PAIRS A such that
A1: b in K and
A2: c in L \/ M and
A3: a = b \/ c by Th34;
( c in L or c in M ) by A2, XBOOLE_0:def 3;
then ( a in K ^ L or a in K ^ M ) by A1, A3, Th35;
hence a in (K ^ L) \/ (K ^ M) by XBOOLE_0:def 3; :: thesis: verum

end;

hence K ^ (L \/ M) c= (K ^ L) \/ (K ^ M) by Lm5; :: according to XBOOLE_0:def 10 :: thesis: (K ^ L) \/ (K ^ M) c= K ^ (L \/ M)
( K ^ L c= K ^ (L \/ M) & K ^ M c= K ^ (L \/ M) ) by Th49, XBOOLE_1:7;
hence (K ^ L) \/ (K ^ M) c= K ^ (L \/ M) by XBOOLE_1:8; :: thesis: verum