let X be set ; :: thesis: for m being Element of MapsT X ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st
( 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 ) )
let m be Element of MapsT X; :: thesis: ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st
( 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 ) )
m in { [[T1,T2],f] where T1, T2 is Element of TOL X, f is Element of FuncsT X : ( ( 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 ) ) } ;
then ex T1, T2 being Element of TOL X ex f being Element of FuncsT X st
( 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 ) ) ;
hence ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st
( 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 ) ) ; :: thesis: verum