reconsider yy = y as Element of B by A1;
deffunc H₁( Element of A) -> Element of [:A,B:] = [$1,yy];
consider f being Function of A,[:A,B:] such that
A2: for x being Element of A holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for x being Element of A holds f . x = [x,y]
thus for x being Element of A holds f . x = [x,y] by A2; :: thesis: verum