theorem :: QUANTAL1:20

for Q being Quantale
for a, b, c being Element of Q st a is dualizing holds
( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a )