set f = id (T `2);

now :: thesis: for x, y being set st [x,y] in T `1 holds
[((id (T `2)) . x),((id (T `2)) . y)] in T `1

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:87;
then A2: (id (T `2)) . x = x by FUNCT_1:18;
y in T `2 by A1, ZFMISC_1:87;
hence [((id (T `2)) . x),((id (T `2)) . y)] in T `1 by A1, A2, FUNCT_1:18; :: thesis: verum

end;

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