let X be set ; :: thesis: for T being Element of TOL X holds
( (id$ T) `2 = id (T `2) & dom (id$ T) = T & cod (id$ T) = T )
let T be Element of TOL X; :: thesis: ( (id$ T) `2 = id (T `2) & dom (id$ T) = T & cod (id$ T) = T )
[[(dom (id$ T)),(cod (id$ T))],((id$ T) `2)] = [[T,T],(id (T `2))] by Th43;
hence ( (id$ T) `2 = id (T `2) & dom (id$ T) = T & cod (id$ T) = T ) by Lm2, ZFMISC_1:27; :: thesis: verum