let X be set ; :: thesis: for f being Function st X c= dom f holds
X -indexing f = f | X
let f be Function; :: thesis: ( X c= dom f implies X -indexing f = f | X )
assume X c= dom f ; :: thesis: X -indexing f = f | X
then A1: dom (f | X) = X by RELAT_1:62;
thus X -indexing f = X -indexing (f | X)
.= f | X by A1, Th10 ; :: thesis: verum