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

let x1, x2 be set ; :: 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 Th22;
A5: ( x1 in dom f & x2 in dom f ) by A3, Th21;
assume A6: (g * f) . x1 = (g * f) . x2 ; :: thesis: x1 = x2
( f . x1 in dom g & f . x2 in dom g ) by A3, Th21;
then f . x1 = f . x2 by A2, A4, A6, Def8;
hence x1 = x2 by A1, A5, Def8; :: thesis: verum

end;

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