let Q be Girard-Quantale; 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; 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 ; ( 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 = (Bottom a) [*] $1;
deffunc H6( Element of Q) -> Element of Q = Bottom $1;
deffunc H7( Element of Q) -> Element of the carrier of Q = (Bottom a) [*] (Bottom $1);
defpred S1[ set ] means $1 in X;
deffunc H8( Element of Q) -> Element of Q = Bottom ((Bottom a) [*] (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; 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 QUANTAL1:sch 1();
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 QUANTAL1:sch 1();
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 FRAENKEL:sch 5(A3);
thus a delta ("/\" (X,Q)) =
Bottom ((Bottom a) [*] ("\/" ( { (Bottom b) where b is Element of Q : b in X } ,Q)))
by Th25
.=
Bottom ("\/" ( { ((Bottom a) [*] (Bottom b)) where b is Element of Q : b in X } ,Q))
by A1, Def5
.=
"/\" ( { (a delta b) where b is Element of Q : b in X } ,Q)
by A2, A4, Th24
; verum