let X be set ; :: thesis: for f being Function holds X -indexing (X -indexing f) = X -indexing f
let f be Function; :: thesis: X -indexing (X -indexing f) = X -indexing f
dom (X -indexing f) = X by PARTFUN1:def 2;
then for x being object st x in X holds
(X -indexing (X -indexing f)) . x = (X -indexing f) . x by Th9;
hence X -indexing (X -indexing f) = X -indexing f by PBOOLE:3; :: thesis: verum