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