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

now

let u, v be Element of Quot. I; :: thesis: F1 . u,v = F2 . u,v
thus F1 . u,v = qmult u,v by A2
.= F2 . u,v by A3 ; :: thesis: verum

end;

hence F1 = F2 by BINOP_1:2; :: thesis: verum