let S be set ; :: thesis: for D1, D2 being non empty set
for f1 being Function of S,D1
for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds
f2 * f1 is bijective
let D1, D2 be non empty set ; :: thesis: for f1 being Function of S,D1
for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds
f2 * f1 is bijective
let f1 be Function of S,D1; :: thesis: for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds
f2 * f1 is bijective
let f2 be Function of D1,D2; :: thesis: ( f1 is bijective & f2 is bijective implies f2 * f1 is bijective )
assume ( f1 is bijective & f2 is bijective ) ; :: thesis: f2 * f1 is bijective
then A1: ( f1 is one-to-one & f1 is onto & f2 is one-to-one & f2 is onto ) ;
set f3 = f2 * f1;
( rng f2 = D2 & rng f1 = D1 & dom f2 = D1 ) by A1, FUNCT_2:def 1, FUNCT_2:def 3;
then rng (f2 * f1) = D2 by RELAT_1:47;
then ( f2 * f1 is one-to-one & f2 * f1 is onto ) by A1, FUNCT_2:def 3;
hence f2 * f1 is bijective ; :: thesis: verum