let f be Function; :: thesis: for A being set st f is one-to-one & A c= bool (dom f) holds
(" f) " A = (.: f) .: A
let A be set ; :: thesis: ( f is one-to-one & A c= bool (dom f) implies (" f) " A = (.: f) .: A )
assume ( f is one-to-one & A c= bool (dom f) ) ; :: thesis: (" f) " A = (.: f) .: A
then ( (" f) " A c= (.: f) .: A & (.: f) .: A c= (" f) " A ) by Th31, Th32;
hence (" f) " A = (.: f) .: A by XBOOLE_0:def 10; :: thesis: verum