let p be Element of REAL 3; :: thesis: for f1, f2, f3 being PartFunc of ,
for t being Real st p = (VFunc f1,f2,f3) . t holds
- p = |[(- (f1 . t)),(- (f2 . t)),(- (f3 . t))]|
let f1, f2, f3 be PartFunc of ,; :: thesis: for t being Real st p = (VFunc f1,f2,f3) . t holds
- p = |[(- (f1 . t)),(- (f2 . t)),(- (f3 . t))]|
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t implies - p = |[(- (f1 . t)),(- (f2 . t)),(- (f3 . t))]| )
assume A1: p = (VFunc f1,f2,f3) . t ; :: thesis: - p = |[(- (f1 . t)),(- (f2 . t)),(- (f3 . t))]|
- p = |[((- 1) * (p . 1)),((- 1) * (p . 2)),((- 1) * (p . 3))]| by Lm3
.= |[(- (p . 1)),(- (p . 2)),(- (p . 3))]|
.= |[(- (f1 . t)),(- (p . 2)),(- (p . 3))]| by A1, Th34
.= |[(- (f1 . t)),(- (f2 . t)),(- (p . 3))]| by A1, Th34
.= |[(- (f1 . t)),(- (f2 . t)),(- (f3 . t))]| by A1, Th34 ;
hence - p = |[(- (f1 . t)),(- (f2 . t)),(- (f3 . t))]| ; :: thesis: verum