let Q be non empty Lattice-like complete right-distributive left-distributive QuantaleStr ; :: thesis: for a, b, c being Element of Q holds
( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) )
let a, b, c be Element of Q; :: thesis: ( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) )
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} } ;
a "\/" b = "\/" {a,b} by LATTICE3:44;
then A1: ( (a "\/" b) [*] c = "\/" { (d [*] c) where d is Element of Q : d in {a,b} } ,Q & c [*] (a "\/" b) = "\/" { (c [*] d) where d is Element of Q : d in {a,b} } ,Q ) by Def5, Def6;

now

let x be set ; :: thesis: ( ( ( x = a [*] c or x = b [*] c ) implies x in { (d [*] c) where d is Element of Q : d in {a,b} } ) & ( not x in { (d [*] c) where d is Element of Q : d in {a,b} } or x = a [*] c or x = b [*] c ) )
( 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: ( not x in { (d [*] c) where d is Element of Q : d in {a,b} } or x = a [*] c or x = b [*] c )
assume x in { (d [*] c) where d is Element of Q : d in {a,b} } ; :: thesis: ( x = a [*] c or x = b [*] c )
then consider d being Element of Q such that
A2: ( x = d [*] c & d in {a,b} ) ;
thus ( x = a [*] c or x = b [*] c ) by A2, TARSKI:def 2; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( ( ( x = c [*] a or x = c [*] b ) implies x in { (c [*] d) where d is Element of Q : d in {a,b} } ) & ( not x in { (c [*] d) where d is Element of Q : d in {a,b} } or x = c [*] a or x = c [*] b ) )
( 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: ( not x in { (c [*] d) where d is Element of Q : d in {a,b} } or x = c [*] a or x = c [*] b )
assume x in { (c [*] d) where d is Element of Q : d in {a,b} } ; :: thesis: ( x = c [*] a or x = c [*] b )
then consider d being Element of Q such that
A3: ( x = c [*] d & d in {a,b} ) ;
thus ( x = c [*] a or x = c [*] b ) by A3, TARSKI:def 2; :: thesis: verum

end;

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