let S be non void Signature; :: thesis: for f, g being Function st g is one-to-one & rng g misses the carrier' of S holds
f,g form_a_replacement_in S
let f, g be Function; :: thesis: ( g is one-to-one & rng g misses the carrier' of S implies f,g form_a_replacement_in S )
assume A1: g is one-to-one ; :: thesis: ( not rng g misses the carrier' of S or f,g form_a_replacement_in S )
assume rng g misses the carrier' of S ; :: thesis: f,g form_a_replacement_in S
then the carrier' of S /\ (rng g) = {} ;
then the carrier' of S /\ (rng g) c= dom g ;
hence f,g form_a_replacement_in S by A1, Th33; :: thesis: verum