set e = the_unity_wrt F;

let u1, u2 be UnOp of D; :: thesis: ( u1 is_an_inverseOp_wrt F & u2 is_an_inverseOp_wrt F implies u1 = u2 )

assume that

A4: for d being Element of D holds

( F . (d,(u1 . d)) = the_unity_wrt F & F . ((u1 . d),d) = the_unity_wrt F ) and

A5: for d being Element of D holds

( F . (d,(u2 . d)) = the_unity_wrt F & F . ((u2 . d),d) = the_unity_wrt F ) ; :: according to FINSEQOP:def 1 :: thesis: u1 = u2

let u1, u2 be UnOp of D; :: thesis: ( u1 is_an_inverseOp_wrt F & u2 is_an_inverseOp_wrt F implies u1 = u2 )

assume that

A4: for d being Element of D holds

( F . (d,(u1 . d)) = the_unity_wrt F & F . ((u1 . d),d) = the_unity_wrt F ) and

A5: for d being Element of D holds

( F . (d,(u2 . d)) = the_unity_wrt F & F . ((u2 . d),d) = the_unity_wrt F ) ; :: according to FINSEQOP:def 1 :: thesis: u1 = u2

now :: thesis: for d being Element of D holds u1 . d = u2 . d

hence
u1 = u2
by FUNCT_2:63; :: thesis: verumlet d be Element of D; :: thesis: u1 . d = u2 . d

set d1 = u1 . d;

set d2 = u2 . d;

thus u1 . d = F . ((u1 . d),(the_unity_wrt F)) by A1, SETWISEO:15

.= F . ((u1 . d),(F . (d,(u2 . d)))) by A5

.= F . ((F . ((u1 . d),d)),(u2 . d)) by A2

.= F . ((the_unity_wrt F),(u2 . d)) by A4

.= u2 . d by A1, SETWISEO:15 ; :: thesis: verum

end;set d1 = u1 . d;

set d2 = u2 . d;

thus u1 . d = F . ((u1 . d),(the_unity_wrt F)) by A1, SETWISEO:15

.= F . ((u1 . d),(F . (d,(u2 . d)))) by A5

.= F . ((F . ((u1 . d),d)),(u2 . d)) by A2

.= F . ((the_unity_wrt F),(u2 . d)) by A4

.= u2 . d by A1, SETWISEO:15 ; :: thesis: verum