let Y, X1, X2 be non empty RelStr ; :: thesis: for f being Function of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds (Proj f,x) . y = f . x,y
let f be Function of [:X1,X2:],Y; :: thesis: for x being Element of X1
for y being Element of X2 holds (Proj f,x) . y = f . x,y
let x be Element of X1; :: thesis: for y being Element of X2 holds (Proj f,x) . y = f . x,y
let y be Element of X2; :: thesis: (Proj f,x) . y = f . x,y
dom f = the carrier of [:X1,X2:] by FUNCT_2:def 1
.= [:the carrier of X1,the carrier of X2:] by YELLOW_3:def 2 ;
then [x,y] in dom f by ZFMISC_1:106;
hence (Proj f,x) . y = f . x,y by FUNCT_5:27; :: thesis: verum