let Q be Quantale; :: thesis: for s, a, b being Element of Q st s is cyclic 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: ( s is cyclic implies ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s )
assume s is cyclic ; :: 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 -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;
{ (a' [*] b') where a', b' is Element of Q : ( a' in H₅(a) & b' in H₅(b) ) } c= H₅(a [*] b)

proof

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

end;

then (a' [*] b') [*] ((a [*] b) -r> s) [= s by A4, LATTICE3:def 21;
hence x in H₅(a [*] b) by A2; :: thesis: verum

end;

hence ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s by A1, LATTICE3:46; :: thesis: verum