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 )
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
deffunc H₅( Element of Q) -> Element of the carrier of Q = $1 [*] (Bottom a);
deffunc H₆( Element of Q) -> Element of Q = Bottom $1;
deffunc H₇( Element of Q) -> Element of the carrier of Q = (Bottom $1) [*] (Bottom a);
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 $1) [*] (Bottom a));
deffunc H₉( Element of Q) -> Element of Q = $1 delta a;
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 ("/\" 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