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₅( Element of Q) -> Element of the carrier of Q = (Bottom a) [*] $1;
deffunc H₆( Element of Q) -> Element of Q = Bottom $1;
deffunc H₇( Element of Q) -> Element of the carrier of Q = (Bottom a) [*] (Bottom $1);
defpred S₁[ set ] means $1 in X;
deffunc H₈( Element of Q) -> Element of Q = Bottom ((Bottom a) [*] (Bottom $1));
deffunc H₉( 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₅(c) where c is Element of Q : c in { H₆(d) where d is Element of Q : S₁[d] } } = { H₅(H₆(b)) where b is Element of Q : S₁[b] } from QUANTAL1:sch 1();
A2: { H₆(c) where c is Element of Q : c in { H₇(d) where d is Element of Q : S₁[d] } } = { H₆(H₇(b)) where b is Element of Q : S₁[b] } from QUANTAL1:sch 1();
A3: for b being Element of Q holds H₈(b) = H₉(b) ;
A4: { H₈(b) where b is Element of Q : S₁[b] } = { H₉(c) where c is Element of Q : S₁[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