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