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 A1: ( f is bijective & g is bijective ) ; :: thesis: ex h being Function of X,Z st
( h = g * f & h is bijective )
then A2: ( f is one-to-one & g is one-to-one ) ;
A3: ( f is onto & g is onto ) by A1;
then A4: rng g = Z by FUNCT_2:def 3;
A5: ( Y = {} iff Z = {} ) by A4;
A6: g * f is one-to-one by A2;
reconsider h = g * f as Function of X,Z by A5;
rng f = Y by A3, FUNCT_2:def 3;
then rng (g * f) = Z by A4, A5, FUNCT_2:20;
then A7: h is onto by FUNCT_2:def 3;
take h ; :: thesis: ( h = g * f & h is bijective )
thus ( h = g * f & h is bijective ) by A6, A7; :: thesis: verum