let X, D be non empty set ; :: thesis: for p being Function of X,D
for i being Element of X holds p /. i = p . i
let p be Function of X,D; :: thesis: for i being Element of X holds p /. i = p . i
let i be Element of X; :: thesis: p /. i = p . i
i in X ;
then i in dom p by Def1;
hence p /. i = p . i by PARTFUN1:def 6; :: thesis: verum