let F1, F2 be UnOp of (Quot. I); :: thesis: ( ( for u being Element of Quot. I holds F1 . u = qaddinv u ) & ( for u being Element of Quot. I holds F2 . u = qaddinv u ) implies F1 = F2 )
assume that
A2: for u being Element of Quot. I holds F1 . u = qaddinv u and
A3: for u being Element of Quot. I holds F2 . u = qaddinv u ; :: thesis: F1 = F2

now

let u be Element of Quot. I; :: thesis: F1 = F2
A4: for u being set st u in Quot. I holds
F1 . u = F2 . u

proof

let u be set ; :: thesis: ( u in Quot. I implies F1 . u = F2 . u )
assume u in Quot. I ; :: thesis: F1 . u = F2 . u
then reconsider u = u as Element of Quot. I ;
F1 . u = qaddinv u by A2
.= F2 . u by A3 ;
hence F1 . u = F2 . u ; :: thesis: verum

end;

( Quot. I = dom F1 & Quot. I = dom F2 ) by FUNCT_2:def 1;
hence F1 = F2 by A4, FUNCT_1:9; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum