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 A1: 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 A2: (id X) . x = x by FUNCT_1:18;
(X -indexing f) . x = ((id X) +* f) . x by A1, Th8;
hence ( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) ) by A2, FUNCT_4:11, FUNCT_4:13; :: thesis: verum