take f = pr1 (D,D); :: thesis: for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds

[(f . (x1,x2)),(f . (y1,y2))] in R

let x1, y1, x2, y2 be Element of D; :: thesis: ( [x1,y1] in R & [x2,y2] in R implies [(f . (x1,x2)),(f . (y1,y2))] in R )

f . (x1,x2) = x1 by FUNCT_3:def 4;

hence ( [x1,y1] in R & [x2,y2] in R implies [(f . (x1,x2)),(f . (y1,y2))] in R ) by FUNCT_3:def 4; :: thesis: verum

[(f . (x1,x2)),(f . (y1,y2))] in R

let x1, y1, x2, y2 be Element of D; :: thesis: ( [x1,y1] in R & [x2,y2] in R implies [(f . (x1,x2)),(f . (y1,y2))] in R )

f . (x1,x2) = x1 by FUNCT_3:def 4;

hence ( [x1,y1] in R & [x2,y2] in R implies [(f . (x1,x2)),(f . (y1,y2))] in R ) by FUNCT_3:def 4; :: thesis: verum