defpred S₁[ set , set ] 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);
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 A2; :: thesis: verum