let G be set ; :: thesis: for H, I being non empty set
for h being Function of G,H
for h1 being Function of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
let H, I be non empty set ; :: thesis: for h being Function of G,H
for h1 being Function of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
let h be Function of G,H; :: thesis: for h1 being Function of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
let h1 be Function of H,I; :: thesis: ( h is bijective & h1 is bijective implies h1 * h is bijective )
assume that
A1: h is bijective and
A2: h1 is bijective ; :: thesis: h1 * h is bijective
( dom h1 = H & rng h = H ) by A1, FUNCT_2:def 3, FUNCT_2:def 1;
then rng (h1 * h) = rng h1 by RELAT_1:28
.= I by A2, FUNCT_2:def 3 ;
hence h1 * h is bijective by A1, A2, FUNCT_2:def 3; :: thesis: verum