let F be Field; :: thesis: for a, b, c being Element of F holds

( a + b = c iff (osf F) . (c,a) = b )

let a, b, c be Element of F; :: thesis: ( a + b = c iff (osf F) . (c,a) = b )

set d = 0. F;

( c + (0. F) = c & (osf F) . (b,(0. F)) = b ) by Th15, REALSET2:2;

hence ( a + b = c iff (osf F) . (c,a) = b ) by Th13; :: thesis: verum

( a + b = c iff (osf F) . (c,a) = b )

let a, b, c be Element of F; :: thesis: ( a + b = c iff (osf F) . (c,a) = b )

set d = 0. F;

( c + (0. F) = c & (osf F) . (b,(0. F)) = b ) by Th15, REALSET2:2;

hence ( a + b = c iff (osf F) . (c,a) = b ) by Th13; :: thesis: verum