let Q be Quantale; :: thesis: 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 )
let a, b, c be Element of Q; :: thesis: ( a is dualizing implies ( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a ) )
deffunc H5( set ) -> set = $1;
defpred S1[ Element of Q] means $1 [*] b [= c;
defpred S2[ Element of Q] means $1 [*] (b [*] (c -l> a)) [= a;
defpred S3[ Element of Q] means b [*] $1 [= c;
defpred S4[ Element of Q] means ((c -r> a) [*] b) [*] $1 [= a;
assume A1: for d being Element of Q holds
( (d -r> a) -l> a = d & (d -l> a) -r> a = d ) ; :: according to QUANTAL1:def 17 :: thesis: ( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a )
then A2: c = (c -l> a) -r> a ;
A3: for d being Element of Q holds
( S1[d] iff S2[d] )
proof
let d be Element of Q; :: thesis: ( S1[d] iff S2[d] )
d [*] (b [*] (c -l> a)) = (d [*] b) [*] (c -l> a) by GROUP_1:def 3;
hence ( S1[d] iff S2[d] ) by A2, Th12; :: thesis: verum
end;
{ H5(d1) where d1 is Element of Q : S1[d1] } = { H5(d2) where d2 is Element of Q : S2[d2] } from FRAENKEL:sch 3(A3);
 hence b -r> c = (b [*] (c -l> a)) -r> a ; :: thesis: b -l> c = ((c -r> a) [*] b) -l> a
A4: c = (c -r> a) -l> a by A1;
A5: for d being Element of Q holds
( S3[d] iff S4[d] )
proof
let d be Element of Q; :: thesis: ( S3[d] iff S4[d] )
((c -r> a) [*] b) [*] d = (c -r> a) [*] (b [*] d) by GROUP_1:def 3;
hence ( S3[d] iff S4[d] ) by A4, Th11; :: thesis: verum
end;
{ H5(d1) where d1 is Element of Q : S3[d1] } = { H5(d2) where d2 is Element of Q : S4[d2] } from FRAENKEL:sch 3(A5);
 hence b -l> c = ((c -r> a) [*] b) -l> a ; :: thesis: verum