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

now :: thesis: for x being object holds
( ( ( 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 ) )

let x be object ; :: 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 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: verum

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: for x being object holds
( ( ( 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 ) )

let x be object ; :: 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 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: verum

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 [*] a) "\/" (c [*] b)
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: verum