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

now :: thesis: for u being Element of Quot. I holds F1 = F2

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

proof

let u be object ; :: 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 = qmultinv u by A2
.= F2 . u by A3 ;
hence F1 . u = F2 . u ; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum