let Q be Quantale; :: thesis: for s, a, b being Element of Q holds ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s
let s, a, b be Element of Q; :: thesis: ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s
deffunc H₅( Element of Q) -> set = { c where c is Element of Q : c [*] ($1 -r> s) [= s } ;
A1: { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H₅(a) & b9 in H₅(b) ) } c= H₅(a [*] b)

proof

defpred S₁[ Element of Q] means $1 [*] (a [*] b) [= s;
deffunc H₆( Element of Q) -> Element of Q = $1;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H₅(a) & b9 in H₅(b) ) } or x in H₅(a [*] b) )
set A = { H₆(c) where c is Element of Q : S₁[c] } ;
assume x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H₅(a) & b9 in H₅(b) ) } ; :: thesis: x in H₅(a [*] b)
then consider a9, b9 being Element of Q such that
A2: x = a9 [*] b9 and
A3: a9 in H₅(a) and
A4: b9 in H₅(b) ;
deffunc H₇( Element of Q) -> Element of the carrier of Q = (a9 [*] b9) [*] $1;
set B = { H₇(H₆(c)) where c is Element of Q : S₁[c] } ;
A5: ex c being Element of Q st
( b9 = c & c [*] (b -r> s) [= s ) by A4;
A6: ex c being Element of Q st
( a9 = c & c [*] (a -r> s) [= s ) by A3;
A7: { H₇(H₆(c)) where c is Element of Q : S₁[c] } is_less_than s

proof

let d be Element of Q; :: according to LATTICE3:def 17 :: thesis: ( not d in { H₇(H₆(c)) where c is Element of Q : S₁[c] } or d [= s )
assume d in { H₇(H₆(c)) where c is Element of Q : S₁[c] } ; :: thesis: d [= s
then consider c being Element of Q such that
A8: d = (a9 [*] b9) [*] c and
A9: c [*] (a [*] b) [= s ;
A10: b -r> s [= b9 -l> s by A5, Th11;
(c [*] a) [*] b [= s by A9, GROUP_1:def 3;
then c [*] a [= b -r> s by Th12;
then c [*] a [= b9 -l> s by A10, LATTICES:7;
then b9 [*] (c [*] a) [= s by Th11;
then (b9 [*] c) [*] a [= s by GROUP_1:def 3;
then A11: b9 [*] c [= a -r> s by Th12;
a -r> s [= a9 -l> s by A6, Th11;
then b9 [*] c [= a9 -l> s by A11, LATTICES:7;
then a9 [*] (b9 [*] c) [= s by Th11;
hence d [= s by A8, GROUP_1:def 3; :: thesis: verum

end;

{ H₇(c) where c is Element of Q : c in { H₆(c) where c is Element of Q : S₁[c] } } = { H₇(H₆(c)) where c is Element of Q : S₁[c] } from QUANTAL1:sch 1();
then (a9 [*] b9) [*] ((a [*] b) -r> s) = "\/" ( { H₇(H₆(c)) where c is Element of Q : S₁[c] } ,Q) by Def5;
then (a9 [*] b9) [*] ((a [*] b) -r> s) [= s by A7, LATTICE3:def 21;
hence x in H₅(a [*] b) by A2; :: thesis: verum

end;

((a -r> s) -r> s) [*] ((b -r> s) -r> s) = "\/" ( { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H₅(a) & b9 in H₅(b) ) } ,Q) by Th5;
hence ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s by A1, LATTICE3:45; :: thesis: verum