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) . 1 = - (f1 . t) & (- p) . 2 = - (f2 . t) & (- p) . 3 = - (f3 . t) )
let f1, f2, f3 be PartFunc of ,; :: thesis: for t being Real st p = (VFunc f1,f2,f3) . t holds
( (- p) . 1 = - (f1 . t) & (- p) . 2 = - (f2 . t) & (- p) . 3 = - (f3 . t) )
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t implies ( (- p) . 1 = - (f1 . t) & (- p) . 2 = - (f2 . t) & (- p) . 3 = - (f3 . t) ) )
assume p = (VFunc f1,f2,f3) . t ; :: thesis: ( (- p) . 1 = - (f1 . t) & (- p) . 2 = - (f2 . t) & (- p) . 3 = - (f3 . t) )
then - p = |[(- (f1 . t)),(- (f2 . t)),(- (f3 . t))]| by Th39;
hence ( (- p) . 1 = - (f1 . t) & (- p) . 2 = - (f2 . t) & (- p) . 3 = - (f3 . t) ) by FINSEQ_1:62; :: thesis: verum