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 :: thesis: for u, v being Element of Quot. I holds F1 . (u,v) = F2 . (u,v)

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