let X, Y be set ; :: thesis: for Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )

let Z be non empty set ; :: thesis: for f being Function of X,Y
for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )

let f be Function of X,Y; :: thesis: for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )

let g be Function of Y,Z; :: thesis: ( f is bijective & g is bijective implies ex h being Function of X,Z st
( h = g * f & h is bijective ) )

assume that
A1: f is bijective and
A2: g is bijective ; :: thesis: ex h being Function of X,Z st
( h = g * f & h is bijective )

A3: rng g = Z by ;
then ( Y = {} iff Z = {} ) ;
then reconsider h = g * f as Function of X,Z ;
take h ; :: thesis: ( h = g * f & h is bijective )
rng f = Y by ;
then rng (g * f) = Z by ;
then h is onto by FUNCT_2:def 3;
hence ( h = g * f & h is bijective ) by A1, A2; :: thesis: verum