reconsider x1 = x as Element of [: the carrier of X, the carrier of Y:] ;
defpred S₁[ Element of X, Element of the carrier of [:X,Y:]] means $2 = [$1,(x1 `2)];
A1: for r being Element of X ex y being Element of the carrier of [:X,Y:] st S₁[r,y]

proof

let r be Element of X; :: thesis: ex y being Element of the carrier of [:X,Y:] st S₁[r,y]
consider p1 being Point of X, p2 being Point of Y such that
X1: x = [p1,p2] by PRVECT_3:18;
[r,(x1 `2)] in [: the carrier of X, the carrier of Y:] by X1, ZFMISC_1:def 2;
hence ex y being Element of the carrier of [:X,Y:] st S₁[r,y] ; :: thesis: verum

end;

ex f being Function of the carrier of X, the carrier of [:X,Y:] st
for r being Element of X holds S₁[r,f . r] from FUNCT_2:sch 3(A1);
hence ex b1 being Function of X,[:X,Y:] st
for r being Element of X holds b1 . r = [r,(x `2)] ; :: thesis: verum