theorem Th13: :: REALSET3:13

for F being Field
for a, b, c, d being Element of F holds
( (osf F) . (a,b) = (osf F) . (c,d) iff a + d = b + c )