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, FUNCT_1:107;
hence f .: ((f ") .: A) = A by A1, FUNCT_1:43; :: thesis: verum