let Y, X2, X1 be non empty RelStr ; :: thesis: for f being Function of [:X1,X2:],Y
for y being Element of X2
for x being Element of X1 holds (Proj f,y) . x = f . x,y
let f be Function of [:X1,X2:],Y; :: thesis: for y being Element of X2
for x being Element of X1 holds (Proj f,y) . x = f . x,y
let y be Element of X2; :: thesis: for x being Element of X1 holds (Proj f,y) . x = f . x,y
let x be Element of X1; :: thesis: (Proj f,y) . x = 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,y) . x = f . x,y by FUNCT_5:29; :: thesis: verum