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_{5}( 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_{5}(a) & b9 in H_{5}(b) ) } c= H_{5}(a [*] b)
_{5}(a) & b9 in H_{5}(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

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

A1: { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H

proof

((a -r> s) -r> s) [*] ((b -r> s) -r> s) = "\/" ( { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H
defpred S_{1}[ Element of Q] means $1 [*] (a [*] b) [= s;

deffunc H_{6}( Element of Q) -> Element of Q = $1;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H_{5}(a) & b9 in H_{5}(b) ) } or x in H_{5}(a [*] b) )

set A = { H_{6}(c) where c is Element of Q : S_{1}[c] } ;

assume x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H_{5}(a) & b9 in H_{5}(b) ) }
; :: thesis: x in H_{5}(a [*] b)

then consider a9, b9 being Element of Q such that

A2: x = a9 [*] b9 and

A3: a9 in H_{5}(a)
and

A4: b9 in H_{5}(b)
;

deffunc H_{7}( Element of Q) -> Element of the carrier of Q = (a9 [*] b9) [*] $1;

set B = { H_{7}(H_{6}(c)) where c is Element of Q : S_{1}[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_{7}(H_{6}(c)) where c is Element of Q : S_{1}[c] } is_less_than s
_{7}(c) where c is Element of Q : c in { H_{6}(c) where c is Element of Q : S_{1}[c] } } = { H_{7}(H_{6}(c)) where c is Element of Q : S_{1}[c] }
from QUANTAL1:sch 1();

then (a9 [*] b9) [*] ((a [*] b) -r> s) = "\/" ( { H_{7}(H_{6}(c)) where c is Element of Q : S_{1}[c] } ,Q)
by Def5;

then (a9 [*] b9) [*] ((a [*] b) -r> s) [= s by A7, LATTICE3:def 21;

hence x in H_{5}(a [*] b)
by A2; :: thesis: verum

end;deffunc H

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H

set A = { H

assume x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H

then consider a9, b9 being Element of Q such that

A2: x = a9 [*] b9 and

A3: a9 in H

A4: b9 in H

deffunc H

set B = { H

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

proof

{ H
let d be Element of Q; :: according to LATTICE3:def 17 :: thesis: ( not d in { H_{7}(H_{6}(c)) where c is Element of Q : S_{1}[c] } or d [= s )

assume d in { H_{7}(H_{6}(c)) where c is Element of Q : S_{1}[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;assume d in { H

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

then (a9 [*] b9) [*] ((a [*] b) -r> s) = "\/" ( { H

then (a9 [*] b9) [*] ((a [*] b) -r> s) [= s by A7, LATTICE3:def 21;

hence x in H

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