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