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)

( 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

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)

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

( 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