let f be Function; :: thesis: for g being one-to-one Function holds (f +* g) * (g ") = id (rng g)
let g be one-to-one Function; :: thesis: (f +* g) * (g ") = id (rng g)
rng (g ") = dom g by FUNCT_1:33;
hence (f +* g) * (g ") = g * (g ") by Th8
.= id (rng g) by FUNCT_1:39 ;
:: thesis: verum