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 H₅( Element of Q) -> Element of the carrier of Q = $1 [*] ("\/" (Y,Q));
deffunc H₆( Element of Q) -> Element of the carrier of Q = "\/" ( { ($1 [*] b) where b is Element of Q : b in Y } ,Q);
defpred S₁[ set ] means $1 in X;
deffunc H₇( Element of Q, Element of Q) -> Element of the carrier of Q = $1 [*] $2;
A1: for a being Element of Q holds H₅(a) = H₆(a) by Def5;
{ H₅(c) where c is Element of Q : S₁[c] } = { H₆(a) where a is Element of Q : S₁[a] } from FRAENKEL:sch 5(A1);
hence ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { ("\/" ( { H₇(a,b) where b is Element of Q : b in Y } ,Q)) where a is Element of Q : a in X } ,Q) by Def6
.= "\/" ( { H₇(c,d) where c, d is Element of Q : ( c in X & d in Y ) } ,Q) from QUANTAL1:sch 3() ;
:: thesis: verum