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