set FV = { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) ) } ;

now :: thesis: ex m being object st m in { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) ) }

set a = [(Total ({} X)),({} X)];
set f = id ([(Total ({} X)),({} X)] `2);
take m = [[[(Total ({} X)),({} X)],[(Total ({} X)),({} X)]],(id ([(Total ({} X)),({} X)] `2))]; :: thesis: m in { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) ) }
reconsider a = [(Total ({} X)),({} X)] as Element of TOL X by Th35;
( a `2 = {} implies a `2 = {} ) ;
then reconsider f = id ([(Total ({} X)),({} X)] `2) as Element of FuncsT X by Th38;
for x, y being set st [x,y] in a `1 holds
[(f . x),(f . y)] in a `1 ;
hence m in { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) ) } ; :: thesis: verum

end;

hence not MapsT X is empty ; :: thesis: verum