let F1, F2 be BinOp of (carr (x,o)); :: thesis: ( ( for a, b being Element of carr (x,o) holds F1 . (a,b) = multR (a,b) ) & ( for a, b being Element of carr (x,o) holds F2 . (a,b) = multR (a,b) ) implies F1 = F2 )

assume that

A2: for a, b being Element of carr (x,o) holds F1 . (a,b) = multR (a,b) and

A3: for a, b being Element of carr (x,o) holds F2 . (a,b) = multR (a,b) ; :: thesis: F1 = F2

assume that

A2: for a, b being Element of carr (x,o) holds F1 . (a,b) = multR (a,b) and

A3: for a, b being Element of carr (x,o) holds F2 . (a,b) = multR (a,b) ; :: thesis: F1 = F2

now :: thesis: for a, b being Element of carr (x,o) holds F1 . (a,b) = F2 . (a,b)

hence
F1 = F2
by BINOP_1:2; :: thesis: verumlet a, b be Element of carr (x,o); :: thesis: F1 . (a,b) = F2 . (a,b)

thus F1 . (a,b) = multR (a,b) by A2

.= F2 . (a,b) by A3 ; :: thesis: verum

end;thus F1 . (a,b) = multR (a,b) by A2

.= F2 . (a,b) by A3 ; :: thesis: verum