let f, g be Function; :: thesis: ( f is one-to-one & g is one-to-one implies g * f is one-to-one )
assume that
A1: f is one-to-one and
A2: g is one-to-one ; :: thesis: g * f is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom (g * f) & x2 in dom (g * f) & (g * f) . x1 = (g * f) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (g * f) & x2 in dom (g * f) & (g * f) . x1 = (g * f) . x2 implies x1 = x2 )
assume A3: ( x1 in dom (g * f) & x2 in dom (g * f) ) ; :: thesis: ( (g * f) . x1 = (g * f) . x2 implies x1 = x2 )
then A4: ( (g * f) . x1 = g . (f . x1) & (g * f) . x2 = g . (f . x2) ) by Th12;
A5: ( x1 in dom f & x2 in dom f ) by A3, Th11;
assume A6: (g * f) . x1 = (g * f) . x2 ; :: thesis: x1 = x2
( f . x1 in dom g & f . x2 in dom g ) by A3, Th11;
then f . x1 = f . x2 by A2, A4, A6;
hence x1 = x2 by A1, A5; :: thesis: verum

end;

hence g * f is one-to-one ; :: thesis: verum