let F be Field; for a, b, c being Element of F holds (osf F) . (a,( the addF of F . (b,c))) = (osf F) . (((osf F) . (a,b)),c)
let a, b, c be Element of F; (osf F) . (a,( the addF of F . (b,c))) = (osf F) . (((osf F) . (a,b)),c)
thus (osf F) . (a,( the addF of F . (b,c))) =
the addF of F . (a,((comp F) . ( the addF of F . (b,c))))
by Def1
.=
a - (b + c)
by VECTSP_1:def 13
.=
(a - b) - c
by RLVECT_1:27
.=
the addF of F . (( the addF of F . (a,(- b))),((comp F) . c))
by VECTSP_1:def 13
.=
the addF of F . (( the addF of F . (a,((comp F) . b))),((comp F) . c))
by VECTSP_1:def 13
.=
the addF of F . (((osf F) . (a,b)),((comp F) . c))
by Def1
.=
(osf F) . (((osf F) . (a,b)),c)
by Def1
; verum