let X be set ; for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2)]
let m be Element of MapsT X; m = [[(dom m),(cod m)],(m `2)]
consider f being Element of FuncsT X, T1, T2 being Element of TOL X such that
A1:
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 Th39;
thus
m = [[(dom m),(cod m)],(m `2)]
by A1; verum