let F1, F2 be BinOp of (rng r); :: thesis: ( ( for a, b being Element of rng r holds F1 . (a,b) = r . (((r ") . a) * ((r ") . b)) ) & ( for a, b being Element of rng r holds F2 . (a,b) = r . (((r ") . a) * ((r ") . b)) ) implies F1 = F2 )

assume that

A2: for a, b being Element of rng r holds F1 . (a,b) = r . (((r ") . a) * ((r ") . b)) and

A3: for a, b being Element of rng r holds F2 . (a,b) = r . (((r ") . a) * ((r ") . b)) ; :: thesis: F1 = F2

assume that

A2: for a, b being Element of rng r holds F1 . (a,b) = r . (((r ") . a) * ((r ") . b)) and

A3: for a, b being Element of rng r holds F2 . (a,b) = r . (((r ") . a) * ((r ") . b)) ; :: thesis: F1 = F2

now :: thesis: for a, b being Element of rng r holds F1 . (a,b) = F2 . (a,b)

hence
F1 = F2
; :: thesis: verumlet a, b be Element of rng r; :: thesis: F1 . (a,b) = F2 . (a,b)

thus F1 . (a,b) = r . (((r ") . a) * ((r ") . b)) by A2

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

end;thus F1 . (a,b) = r . (((r ") . a) * ((r ") . b)) by A2

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