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 Th15
.= (osf F) . (a * c),(b * c)
.= (osf F) . ((omf F) . a,c),((omf F) . b,c) ; :: thesis: verum