let f be Function; :: thesis: for A being set st f is one-to-one & A c= dom (f " ) holds
f .: ((f " ) .: A) = A
let A be set ; :: thesis: ( f is one-to-one & A c= dom (f " ) implies f .: ((f " ) .: A) = A )
assume that
A1: f is one-to-one and
A2: A c= dom (f " ) ; :: thesis: f .: ((f " ) .: A) = A
((f " ) " ) .: ((f " ) .: A) = A by A1, A2, JGRAPH_6:22;
hence f .: ((f " ) .: A) = A by A1, FUNCT_1:65; :: thesis: verum