consider f being Element of FuncsT X, T1, T2 being Element of TOL X such that
A1: ( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) ) by Th39;
thus for b₁ being set st b₁ = m `2 holds
( b₁ is Function-like & b₁ is Relation-like ) by A1; :: thesis: verum