let X be set ; :: thesis: for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2 )]
let m be Element of MapsT X; :: thesis: 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 Th41;
[T1,T2] = m `1 by A1, MCART_1:def 1;
then m `1 = [(dom m),(cod m)] by MCART_1:8;
hence m = [[(dom m),(cod m)],(m `2 )] by A1, MCART_1:8; :: thesis: verum