let V be non empty set ; :: thesis: for A being Element of V holds
( (id$ A) `2 = id A & dom (id$ A) = A & cod (id$ A) = A )
let A be Element of V; :: thesis: ( (id$ A) `2 = id A & dom (id$ A) = A & cod (id$ A) = A )
[[(dom (id$ A)),(cod (id$ A))],((id$ A) `2 )] = [[A,A],(id A)] by Th8;
hence ( (id$ A) `2 = id A & dom (id$ A) = A & cod (id$ A) = A ) by Lm1, ZFMISC_1:33; :: thesis: verum