defpred S₁[ 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 S₁[x,y] ;
consider F being Function of REAL,(REAL 3) such that
A2: for t being Element of REAL holds S₁[t,F . t] from FUNCT_2:sch 3(A1);
A3: for t being Real holds S₁[t,F . t]

proof

let t be Real; :: thesis: S₁[t,F . t]
reconsider t = t as Element of REAL by XREAL_0:def 1;
S₁[t,F . t] by A2;
hence S₁[t,F . t] ; :: thesis: verum

end;

take F ; :: thesis: 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; :: thesis: verum