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

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:23
.= F . (u1 . d),(F . d,(u2 . d)) by A5
.= F . (F . (u1 . d),d),(u2 . d) by A2, BINOP_1:def 3
.= F . (the_unity_wrt F),(u2 . d) by A4
.= u2 . d by A1, SETWISEO:23 ; :: thesis: verum

end;

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