let F be Field; :: thesis: for a, b, c being Element of F holds (omf F) . (((osf F) . (a,b)),c) = (osf F) . (((omf F) . (a,c)),((omf F) . (b,c)))
let a, b, c be Element of F; :: thesis: (omf F) . (((osf F) . (a,b)),c) = (osf F) . (((omf F) . (a,c)),((omf F) . (b,c)))
thus (omf F) . (((osf F) . (a,b)),c) = ((osf F) . (a,b)) * c
.= c * ((osf F) . (a,b))
.= (omf F) . (c,((osf F) . (a,b)))
.= (osf F) . ((c * a),(c * b)) by Th9
.= (osf F) . ((a * c),(b * c))
.= (osf F) . (((omf F) . (a,c)),((omf F) . (b,c))) ; :: thesis: verum