a1: ( dom H = [:Y,Y:] & dom f = X & dom g = X ) by FUNCT_2:def 1;
a2: rng [:f,g:] c= [:Y,Y:] ;
dom (H * (f,g)) = dom (H * [:f,g:]) by FINSEQOP:def 4;
then dom (H * (f,g)) = dom [:f,g:] by a1, a2, RELAT_1:27;
then a3: dom (H * (f,g)) = [:X,X:] by FUNCT_2:def 1;
rng (H * (f,g)) = rng (H * [:f,g:]) by FINSEQOP:def 4;
then ( rng (H * (f,g)) c= rng H & rng H c= Y ) by RELAT_1:26, RELAT_1:def 19;
hence H * (f,g) is Function of [:X,X:],Y by a3, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum