let X1, X2, Y 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:87;
hence (Proj (f,x)) . y = f . (x,y) by FUNCT_5:20; :: thesis: verum