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

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

let X be set ; :: thesis: ( a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) & a delta ("/\" (X,Q)) = "/\" ( { (a delta c) 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 = a delta \$1;
thus a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) by Def5; :: thesis: a delta ("/\" (X,Q)) = "/\" ( { (a delta c) 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 a delta ("/\" (X,Q)) = 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
.= "/\" ( { (a delta b) where b is Element of Q : b in X } ,Q) by A2, A4, Th24 ; :: thesis: verum