theorem :: QUANTAL1:28

for Q being Girard-Quantale
for a being Element of Q
for X being set holds
( ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) & ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q) )