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 )
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
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;
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();
deffunc H₈( Element of Q) -> Element of Q = Bottom ((Bottom a) [*] (Bottom $1));
deffunc H₉( Element of Q) -> Element of Q = a delta $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