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_{5}( Element of Q) -> Element of the carrier of Q = $1 [*] ("\/" (Y,Q));

deffunc H_{6}( Element of Q) -> Element of the carrier of Q = "\/" ( { ($1 [*] b) where b is Element of Q : b in Y } ,Q);

defpred S_{1}[ set ] means $1 in X;

deffunc H_{7}( Element of Q, Element of Q) -> Element of the carrier of Q = $1 [*] $2;

A1: for a being Element of Q holds H_{5}(a) = H_{6}(a)
by Def5;

{ H_{5}(c) where c is Element of Q : S_{1}[c] } = { H_{6}(a) where a is Element of Q : S_{1}[a] }
from FRAENKEL:sch 5(A1);

hence ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { ("\/" ( { H_{7}(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_{7}(c,d) where c, d is Element of Q : ( c in X & d in Y ) } ,Q)
from QUANTAL1:sch 3()
;

:: thesis: verum

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

deffunc H

defpred S

deffunc H

A1: for a being Element of Q holds H

{ H

hence ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { ("\/" ( { H

.= "\/" ( { H

:: thesis: verum