let E, F, G be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for x1 being Point of E
for x2 being Point of F
for x3 being Point of G holds - [x1,x2,x3] = [(- x1),(- x2),(- x3)]
let x1 be Point of E; :: thesis: for x2 being Point of F
for x3 being Point of G holds - [x1,x2,x3] = [(- x1),(- x2),(- x3)]
let x2 be Point of F; :: thesis: for x3 being Point of G holds - [x1,x2,x3] = [(- x1),(- x2),(- x3)]
let x3 be Point of G; :: thesis: - [x1,x2,x3] = [(- x1),(- x2),(- x3)]
thus - [x1,x2,x3] = [(- [x1,x2]),(- x3)] by PRVECT_3:8
.= [(- x1),(- x2),(- x3)] by PRVECT_3:8 ; :: thesis: verum