set e = the_unity_wrt F;
let u1, u2 be UnOp of D; :: thesis:
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:

let d be Element of D; :: thesis:
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:

end;