set f = id (T `2 );

now

let x, y be set ; :: thesis: ( [x,y] in T `1 implies [((id (T `2 )) . x),((id (T `2 )) . y)] in T `1 )
assume A1: [x,y] in T `1 ; :: thesis: [((id (T `2 )) . x),((id (T `2 )) . y)] in T `1
then x in T `2 by ZFMISC_1:106;
then A2: (id (T `2 )) . x = x by FUNCT_1:35;
y in T `2 by A1, ZFMISC_1:106;
hence [((id (T `2 )) . x),((id (T `2 )) . y)] in T `1 by A1, A2, FUNCT_1:35; :: thesis: verum

end;

hence [[T,T],(id (T `2 ))] is Element of MapsT X by Th42; :: thesis: verum