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

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