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