let F, G be Function of REAL,(REAL 3); :: thesis: ( ( for t being Real holds F . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) & ( for t being Real holds G . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) implies F = G )
assume that
A4: for t being Real holds F . t = |[(f1 . t),(f2 . t),(f3 . t)]| and
A5: for t being Real holds G . t = |[(f1 . t),(f2 . t),(f3 . t)]| ; :: thesis: F = G

now :: thesis: for t being Element of REAL holds F . t = G . t

let t be Element of REAL ; :: thesis: F . t = G . t
F . t = |[(f1 . t),(f2 . t),(f3 . t)]| by A4;
hence F . t = G . t by A5; :: thesis: verum

end;

hence F = G by FUNCT_2:63; :: thesis: verum