let X be set ; :: thesis: for A being Subset of X holds (id X) .: A = A
let A be Subset of X; :: thesis: (id X) .: A = A

now

let e be set ; :: thesis: ( ( e in A implies ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) ) & ( ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) implies e in A ) )
A1: dom (id X) = X by Th34;
thus ( e in A implies ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) ) :: thesis: ( ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) implies e in A )

proof

assume A2: e in A ; :: thesis: ex u being set st
( u in dom (id X) & u in A & e = (id X) . u )
take e ; :: thesis: ( e in dom (id X) & e in A & e = (id X) . e )
thus e in dom (id X) by A1, A2; :: thesis: ( e in A & e = (id X) . e )
thus e in A by A2; :: thesis: e = (id X) . e
thus e = (id X) . e by A2, Th34; :: thesis: verum

end;

assume ex u being set st
( u in dom (id X) & u in A & e = (id X) . u ) ; :: thesis: e in A
hence e in A by Th34; :: thesis: verum

end;

hence (id X) .: A = A by Def12; :: thesis: verum