let Q be non empty Lattice-like complete right-distributive left-distributive QuantaleStr ; 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 ; ("\/" (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 FRAENKEL:sch 5(A1);
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 QUANTAL1:sch 3()
;
verum