let X, x be set ; :: thesis: for f being Function st x in X holds
( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) )
let f be Function; :: thesis: ( x in X implies ( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) ) )
assume x in X ; :: thesis: ( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) )
then ( (X -indexing f) . x = ((id X) +* f) . x & dom (id X) = X & (id X) . x = x ) by Th8, FUNCT_1:35, RELAT_1:71;
hence ( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) ) by FUNCT_4:12, FUNCT_4:14; :: thesis: verum