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

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

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

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

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

deffunc H_{9}( 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: { 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 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 ; :: thesis: verum

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 H

deffunc H

deffunc H

defpred S

deffunc H

deffunc H

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

A2: { H

A3: for b being Element of Q holds H

A4: { H

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