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 )
set f3 = f2 * f1;
A1: dom f2 = D1 by FUNCT_2:def 1;
assume A2: ( f1 is bijective & f2 is bijective ) ; :: thesis: f2 * f1 is bijective
then ( rng f2 = D2 & rng f1 = D1 ) by FUNCT_2:def 3;
then rng (f2 * f1) = D2 by A1, RELAT_1:28;
then ( f2 * f1 is one-to-one & f2 * f1 is onto ) by A2, FUNCT_2:def 3;
hence f2 * f1 is bijective ; :: thesis: verum