let Q be non empty Lattice-like complete right-distributive left-distributive QuantaleStr ; 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; ( (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} } ;
then A1:
{ (d [*] c) where d is Element of Q : d in {a,b} } = {(a [*] c),(b [*] c)}
by TARSKI:def 2;
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; 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; verum