let Q be non empty Lattice-like complete right-distributive left-distributive QuantaleStr ; :: thesis: for X, Y being set holds ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q)
let X, Y be set ; :: thesis: ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q)
deffunc H5( Element of Q) -> Element of the carrier of Q = \$1 [*] ("\/" (Y,Q));
deffunc H6( Element of Q) -> Element of the carrier of Q = "\/" ( { (\$1 [*] b) where b is Element of Q : b in Y } ,Q);
defpred S1[ set ] means \$1 in X;
deffunc H7( Element of Q, Element of Q) -> Element of the carrier of Q = \$1 [*] \$2;
A1: for a being Element of Q holds H5(a) = H6(a) by Def5;
{ H5(c) where c is Element of Q : S1[c] } = { H6(a) where a is Element of Q : S1[a] } from hence ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { ("\/" ( { H7(a,b) where b is Element of Q : b in Y } ,Q)) where a is Element of Q : a in X } ,Q) by Def6
.= "\/" ( { H7(c,d) where c, d is Element of Q : ( c in X & d in Y ) } ,Q) from ;
:: thesis: verum