set h = <:f,g:>;

now :: thesis: for x1, x2 being object st x1 in dom <:f,g:> & x2 in dom <:f,g:> & <:f,g:> . x1 = <:f,g:> . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom <:f,g:> & x2 in dom <:f,g:> & <:f,g:> . x1 = <:f,g:> . x2 implies x1 = x2 )
assume A1: ( x1 in dom <:f,g:> & x2 in dom <:f,g:> & <:f,g:> . x1 = <:f,g:> . x2 ) ; :: thesis: x1 = x2
then ( x1 in (dom f) /\ (dom g) & x2 in (dom f) /\ (dom g) ) by FUNCT_3:def 7;
then A2: ( x1 in dom g & x2 in dom g ) by XBOOLE_0:def 4;
( [(f . x1),(g . x1)] = <:f,g:> . x1 & [(f . x2),(g . x2)] = <:f,g:> . x2 ) by A1, FUNCT_3:def 7;
then g . x1 = g . x2 by A1, XTUPLE_0:1;
hence x1 = x2 by A2, FUNCT_1:def 4; :: thesis: verum

end;

hence <:f,g:> is one-to-one by FUNCT_1:def 4; :: thesis: verum