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 H₅( set ) -> set = $1;
defpred S₁[ Element of Q] means $1 [*] b [= c;
defpred S₂[ Element of Q] means $1 [*] (b [*] (c -l> a)) [= a;
defpred S₃[ Element of Q] means b [*] $1 [= c;
defpred S₄[ 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
( S₁[d] iff S₂[d] )

proof

let d be Element of Q; :: thesis: ( S₁[d] iff S₂[d] )
d [*] (b [*] (c -l> a)) = (d [*] b) [*] (c -l> a) by GROUP_1:def 3;
hence ( S₁[d] iff S₂[d] ) by A2, Th12; :: thesis: verum

end;

{ H₅(d1) where d1 is Element of Q : S₁[d1] } = { H₅(d2) where d2 is Element of Q : S₂[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
( S₃[d] iff S₄[d] )

proof

let d be Element of Q; :: thesis: ( S₃[d] iff S₄[d] )
((c -r> a) [*] b) [*] d = (c -r> a) [*] (b [*] d) by GROUP_1:def 3;
hence ( S₃[d] iff S₄[d] ) by A4, Th11; :: thesis: verum

end;

{ H₅(d1) where d1 is Element of Q : S₃[d1] } = { H₅(d2) where d2 is Element of Q : S₄[d2] } from FRAENKEL:sch 3(A5);
hence b -l> c = ((c -r> a) [*] b) -l> a ; :: thesis: verum