let X, Y be set ; :: thesis: for f being Function st X c= Y holds
(Y -indexing f) | X = X -indexing f
let f be Function; :: thesis: ( X c= Y implies (Y -indexing f) | X = X -indexing f )
assume A1: X c= Y ; :: thesis: (Y -indexing f) | X = X -indexing f
then A2: (f | Y) | X = f | X by RELAT_1:74;
(id Y) | X = id X by A1, FUNCT_3:1;
hence (Y -indexing f) | X = X -indexing f by A2, FUNCT_4:71; :: thesis: verum