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

( 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