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

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 Th37;
A1: ( a `2 = {} implies a `2 = {} ) ;
then reconsider f = id ([(Total ({} X)),({} X)] `2) as Element of FuncsT X by Th40;

now

let x, y be set ; :: thesis: ( [x,y] in a `1 implies [(f . x),(f . y)] in a `1 )
assume A2: [x,y] in a `1 ; :: thesis: [(f . x),(f . y)] in a `1
then x in a `2 by ZFMISC_1:87;
then A3: f . x = x by FUNCT_1:18;
y in a `2 by A2, ZFMISC_1:87;
hence [(f . x),(f . y)] in a `1 by A2, A3, FUNCT_1:18; :: thesis: verum

end;

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 ) ) } by A1; :: thesis: verum

end;

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