let F be Field; :: thesis: for a being Element of F holds (osf F) . ((0. F),a) = (comp F) . a
let a be Element of F; :: thesis: (osf F) . ((0. F),a) = (comp F) . a
thus (osf F) . ((0. F),a) = (0. F) + ((comp F) . a) by Def1
.= (comp F) . a by REALSET2:2 ; :: thesis: verum