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

end;

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