defpred S1[ object , object ] means $2 = |[(f1 . $1),(f2 . $1),(f3 . $1)]|;
A1:
for x being Element of REAL ex y being Element of REAL 3 st S1[x,y]
;
consider F being Function of REAL,(REAL 3) such that
A2:
for t being Element of REAL holds S1[t,F . t]
from FUNCT_2:sch 3(A1);
A3:
for t being Real holds S1[t,F . t]
take
F
; for t being Real holds F . t = |[(f1 . t),(f2 . t),(f3 . t)]|
thus
for t being Real holds F . t = |[(f1 . t),(f2 . t),(f3 . t)]|
by A3; verum