If f : A -> B and g : B -> C for some sets A, B, C, then the composition g o f : A -> C exists regardless of the particular definitions of f and g. The definition of the composition proves its existence; there is no issue here that requires proving that composition is well-defined.