let Q be Quantale; :: thesis: for D being Element of Q st D is dualizing holds
( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )
let D be Element of Q; :: thesis: ( D is dualizing implies ( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) )
set I = D -l> D;
set J = D -r> D;
assume A1: for a being Element of Q holds
( (a -r> D) -l> D = a & (a -l> D) -r> D = a ) ; :: according to QUANTAL1:def 17 :: thesis: ( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )

A2: now :: thesis: for a being Element of Q holds
( a [*] (D -l> D) = a & (D -r> D) [*] a = a )

deffunc H₅( set ) -> set = $1;
let a be Element of Q; :: thesis: ( a [*] (D -l> D) = a & (D -r> D) [*] a = a )
defpred S₁[ Element of Q] means $1 [*] (a [*] (D -l> D)) [= D;
defpred S₂[ Element of Q] means $1 [*] a [= D;
defpred S₃[ Element of Q] means ((D -r> D) [*] a) [*] $1 [= D;
defpred S₄[ Element of Q] means a [*] $1 [= D;
A3: for b being Element of Q holds
( S₁[b] iff S₂[b] )

proof

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

end;

A4: { H₅(b) where b is Element of Q : S₁[b] } = { H₅(c) where c is Element of Q : S₂[c] } from FRAENKEL:sch 3(A3);
thus a [*] (D -l> D) = ((a [*] (D -l> D)) -r> D) -l> D by A1
.= (a -r> D) -l> D by A4
.= a by A1 ; :: thesis: (D -r> D) [*] a = a
A5: for b being Element of Q holds
( S₃[b] iff S₄[b] )

proof

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

end;

A6: { H₅(b) where b is Element of Q : S₃[b] } = { H₅(c) where c is Element of Q : S₄[c] } from FRAENKEL:sch 3(A5);
thus (D -r> D) [*] a = (((D -r> D) [*] a) -l> D) -r> D by A1
.= (a -l> D) -r> D by A6
.= a by A1 ; :: thesis: verum

end;

A7: D -l> D is_a_right_unity_wrt H₄(Q)

proof

let a be Element of Q; :: according to BINOP_1:def 17 :: thesis: H₄(Q) . (a,(D -l> D)) = a
thus H₄(Q) . (a,(D -l> D)) = a [*] (D -l> D)
.= a by A2 ; :: thesis: verum

end;

A8: D -l> D = (D -r> D) [*] (D -l> D) by A2;
D -l> D is_a_left_unity_wrt H₄(Q)

proof

let a be Element of Q; :: according to BINOP_1:def 16 :: thesis: H₄(Q) . ((D -l> D),a) = a
thus H₄(Q) . ((D -l> D),a) = (D -r> D) [*] a by A2, A8
.= a by A2 ; :: thesis: verum

end;

then A9: D -l> D is_a_unity_wrt H₄(Q) by A7;
hence H₄(Q) is having_a_unity ; :: according to MONOID_0:def 10 :: thesis: ( the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )
D -r> D = (D -r> D) [*] (D -l> D) by A2;
hence ( the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) by A8, A9, BINOP_1:def 8; :: thesis: verum