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

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

let 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;

hence u1 = u2 by FUNCT_2:63; :: thesis: verum