let X be set ; :: thesis: for f being Function st X in dom (.: f) holds
(.: f) . X = f .: X
let f be Function; :: thesis: ( X in dom (.: f) implies (.: f) . X = f .: X )
assume X in dom (.: f) ; :: thesis: (.: f) . X = f .: X
then X in bool (dom f) by Def1;
hence (.: f) . X = f .: X by Def1; :: thesis: verum