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 X c= Y ; :: thesis: (Y -indexing f) | X = X -indexing f
then ( (id Y) | X = id X & (f | Y) | X = f | X & X -indexing f = (id X) +* (f | X) & Y -indexing f = (id Y) +* (f | Y) ) by FUNCT_3:1, RELAT_1:103;
hence (Y -indexing f) | X = X -indexing f by FUNCT_4:75; :: thesis: verum