let Q be Girard-Quantale; :: thesis: 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) )

let a be Element of Q; :: thesis: 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) )

let X be set ; :: thesis: ( ("\/" (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) )
deffunc H5( Element of Q) -> Element of the carrier of Q = \$1 [*] ();
deffunc H6( Element of Q) -> Element of Q = Bottom \$1;
deffunc H7( Element of Q) -> Element of the carrier of Q = (Bottom \$1) [*] ();
defpred S1[ set ] means \$1 in X;
deffunc H8( Element of Q) -> Element of Q = Bottom ((Bottom \$1) [*] ());
deffunc H9( Element of Q) -> Element of Q = \$1 delta a;
thus ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) by Def6; :: thesis: ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q)
A1: { H5(c) where c is Element of Q : c in { H6(d) where d is Element of Q : S1[d] } } = { H5(H6(b)) where b is Element of Q : S1[b] } from A2: { H6(c) where c is Element of Q : c in { H7(d) where d is Element of Q : S1[d] } } = { H6(H7(b)) where b is Element of Q : S1[b] } from A3: for b being Element of Q holds H8(b) = H9(b) ;
A4: { H8(b) where b is Element of Q : S1[b] } = { H9(c) where c is Element of Q : S1[c] } from thus ("/\" (X,Q)) delta a = Bottom (("\/" ( { () where b is Element of Q : b in X } ,Q)) [*] ()) by Th25
.= Bottom ("\/" ( { (() [*] ()) where b is Element of Q : b in X } ,Q)) by
.= "/\" ( { (b delta a) where b is Element of Q : b in X } ,Q) by A2, A4, Th24 ; :: thesis: verum