let A, B be non empty set ; :: thesis: for f being Function of A,B
for x being Element of A
for y being set holds (f +* (x,y)) . x = y
let f be Function of A,B; :: thesis: for x being Element of A
for y being set holds (f +* (x,y)) . x = y
let x be Element of A; :: thesis: for y being set holds (f +* (x,y)) . x = y
let y be set ; :: thesis: (f +* (x,y)) . x = y
x in A ;
then x in dom f by FUNCT_2:def 1;
hence (f +* (x,y)) . x = y by Th30; :: thesis: verum