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 H_{5}( Element of Q) -> Element of the carrier of Q = $1 [*] (Bottom a);

deffunc H_{6}( Element of Q) -> Element of Q = Bottom $1;

deffunc H_{7}( Element of Q) -> Element of the carrier of Q = (Bottom $1) [*] (Bottom a);

defpred S_{1}[ set ] means $1 in X;

deffunc H_{8}( Element of Q) -> Element of Q = Bottom ((Bottom $1) [*] (Bottom a));

deffunc H_{9}( 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: { H_{5}(c) where c is Element of Q : c in { H_{6}(d) where d is Element of Q : S_{1}[d] } } = { H_{5}(H_{6}(b)) where b is Element of Q : S_{1}[b] }
from QUANTAL1:sch 1();

A2: { H_{6}(c) where c is Element of Q : c in { H_{7}(d) where d is Element of Q : S_{1}[d] } } = { H_{6}(H_{7}(b)) where b is Element of Q : S_{1}[b] }
from QUANTAL1:sch 1();

A3: for b being Element of Q holds H_{8}(b) = H_{9}(b)
;

A4: { H_{8}(b) where b is Element of Q : S_{1}[b] } = { H_{9}(c) where c is Element of Q : S_{1}[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 ; :: thesis: verum

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 H

deffunc H

deffunc H

defpred S

deffunc H

deffunc H

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: { H

A2: { H

A3: for b being Element of Q holds H

A4: { H

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 ; :: thesis: verum