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: { (a' [*] b') where a', b' is Element of Q : ( a' in H₅(a) & b' 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 { (a' [*] b') where a', b' is Element of Q : ( a' in H₅(a) & b' in H₅(b) ) } or x in H₅(a [*] b) )
set A = { H₆(c) where c is Element of Q : S₁[c] } ;
assume x in { (a' [*] b') where a', b' is Element of Q : ( a' in H₅(a) & b' in H₅(b) ) } ; :: thesis: x in H₅(a [*] b)
then consider a', b' being Element of Q such that
A2: x = a' [*] b' and
A3: a' in H₅(a) and
A4: b' in H₅(b) ;
deffunc H₇( Element of Q) -> Element of the carrier of Q = (a' [*] b') [*] $1;
set B = { H₇(H₆(c)) where c is Element of Q : S₁[c] } ;
A5: ex c being Element of Q st
( b' = c & c [*] (b -r> s) [= s ) by A4;
A6: ex c being Element of Q st
( a' = 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 = (a' [*] b') [*] c and
A9: c [*] (a [*] b) [= s ;
A10: b -r> s [= b' -l> s by A5, Th11;
(c [*] a) [*] b [= s by A9, GROUP_1:def 4;
then c [*] a [= b -r> s by Th12;
then c [*] a [= b' -l> s by A10, LATTICES:25;
then b' [*] (c [*] a) [= s by Th11;
then (b' [*] c) [*] a [= s by GROUP_1:def 4;
then A11: b' [*] c [= a -r> s by Th12;
a -r> s [= a' -l> s by A6, Th11;
then b' [*] c [= a' -l> s by A11, LATTICES:25;
then a' [*] (b' [*] c) [= s by Th11;
hence d [= s by A8, GROUP_1:def 4; :: 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 (a' [*] b') [*] ((a [*] b) -r> s) = "\/" { H₇(H₆(c)) where c is Element of Q : S₁[c] } ,Q by Def5;
then (a' [*] b') [*] ((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) = "\/" { (a' [*] b') where a', b' is Element of Q : ( a' in H₅(a) & b' 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:46; :: thesis: verum