let X be non empty set ; :: thesis: for f being Function
for x being Element of X holds (X -indexing f) . x = ((id X) +* f) . x
let f be Function; :: thesis: for x being Element of X holds (X -indexing f) . x = ((id X) +* f) . x
let x be Element of X; :: thesis: (X -indexing f) . x = ((id X) +* f) . x
((id X) +* f) | X = ((id X) | X) +* (f | X) by FUNCT_4:71
.= ((id X) | (dom (id X))) +* (f | X)
.= X -indexing f ;
hence (X -indexing f) . x = ((id X) +* f) . x by FUNCT_1:49; :: thesis: verum