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