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

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

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

then A1:
{ (d [*] c) where d is Element of Q : d in {a,b} } = {(a [*] c),(b [*] c)}
by TARSKI:def 2;( ( ( 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;( 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

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

then A2:
{ (c [*] d) where d is Element of Q : d in {a,b} } = {(c [*] a),(c [*] b)}
by TARSKI:def 2;( ( ( 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;( 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

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