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

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