let Q be non empty Lattice-like complete right-distributive left-distributive QuantaleStr ; :: thesis:
let a, b, c be Element of Q; :: thesis:
set X1 = { (d [*] c) where d is Element of Q : d in {a,b} } ;
set X2 = { (c [*] d) where d is Element of Q : d in {a,b} } ;

now :: thesis:

let x be object ; :: thesis:
( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
hence ( ( x = a [*] c or x = b [*] c ) implies x in { (d [*] c) where d is Element of Q : d in {a,b} } ) ; :: thesis:
assume x in { (d [*] c) where d is Element of Q : d in {a,b} } ; :: thesis:
then ex d being Element of Q st
( x = d [*] c & d in {a,b} ) ;
hence ( x = a [*] c or x = b [*] c ) by TARSKI:def 2; :: thesis:

end;

then A1: { (d [*] c) where d is Element of Q : d in {a,b} } = {(a [*] c),(b [*] c)} by TARSKI:def 2;

now :: thesis:

let x be object ; :: thesis:
( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
hence ( ( x = c [*] a or x = c [*] b ) implies x in { (c [*] d) where d is Element of Q : d in {a,b} } ) ; :: thesis:
assume x in { (c [*] d) where d is Element of Q : d in {a,b} } ; :: thesis:
then ex d being Element of Q st
( x = c [*] d & d in {a,b} ) ;
hence ( x = c [*] a or x = c [*] b ) by TARSKI:def 2; :: thesis:

end;

then A2: { (c [*] d) where d is Element of Q : d in {a,b} } = {(c [*] a),(c [*] b)} by TARSKI:def 2;
A3: a "\/" b = "\/" {a,b} by LATTICE3:43;
then (a "\/" b) [*] c = "\/" ( { (d [*] c) where d is Element of Q : d in {a,b} } ,Q) by Def6;
hence (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) by A1, LATTICE3:43; :: thesis:
c [*] (a "\/" b) = "\/" ( { (c [*] d) where d is Element of Q : d in {a,b} } ,Q) by A3, Def5;
hence c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) by A2, LATTICE3:43; :: thesis: