take f = pr2 (C,D); :: thesis: for x being Element of C
for y1, y2 being Element of D st [y1,y2] in R holds
[(f . (x,y1)),(f . (x,y2))] in R
let x be Element of C; :: thesis: for y1, y2 being Element of D st [y1,y2] in R holds
[(f . (x,y1)),(f . (x,y2))] in R
let y1, y2 be Element of D; :: thesis: ( [y1,y2] in R implies [(f . (x,y1)),(f . (x,y2))] in R )
f . (x,y1) = y1 by FUNCT_3:def 5;
hence ( [y1,y2] in R implies [(f . (x,y1)),(f . (x,y2))] in R ) by FUNCT_3:def 5; :: thesis: verum