let F be Field; :: thesis: for a, b, c being Element of F holds
( a + b = c iff (osf F) . (c,b) = a )
let a, b, c be Element of F; :: thesis: ( a + b = c iff (osf F) . (c,b) = a )
set d = 0. F;
( c + (0. F) = c & (osf F) . (a,(0. F)) = a ) by Th15, REALSET2:2;
hence ( a + b = c iff (osf F) . (c,b) = a ) by Th13; :: thesis: verum