consider f being Element of FuncsT X, T1, T2 being Element of TOL X such that
A2: m = [[T1,T2],f] and
( T2 `2 = {} implies T1 `2 = {} ) and
f is Function of (T1 `2),(T2 `2) and
for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 by Th40;
( [T1,T2] = [[T1,T2],f] `1 & [T1,T2] `2 = T2 ) ;
hence (m `1) `2 is Element of TOL X by A2; :: thesis: verum