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 A2, FUNCT_2:def 3;

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 A1, FUNCT_2:def 3;

then rng (g * f) = Z by A3, FUNCT_2:14;

then h is onto by FUNCT_2:def 3;

hence ( h = g * f & h is bijective ) by A1, A2; :: thesis: verum

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 A2, FUNCT_2:def 3;

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 A1, FUNCT_2:def 3;

then rng (g * f) = Z by A3, FUNCT_2:14;

then h is onto by FUNCT_2:def 3;

hence ( h = g * f & h is bijective ) by A1, A2; :: thesis: verum