reconsider yy = y as Element of B by A1;

deffunc H_{1}( 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_{1}(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

deffunc H

consider f being Function of A,[:A,B:] such that

A2: for x being Element of A holds f . x = H

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