[x,y] is set by TARSKI:1;
then reconsider z = [x,y] as Point of [:E,F:] by PRVECT_3:9;
f . z is Point of G ;
hence f . (x,y) is Point of G ; :: thesis: verum