let T be 1-sorted ; :: thesis: for S, V being non empty 1-sorted
for f being Function of T,S
for g being Function of S,V st rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds
(g * f) " = (f ") * (g ")
let S, V be non empty 1-sorted ; :: thesis: for f being Function of T,S
for g being Function of S,V st rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds
(g * f) " = (f ") * (g ")
let f be Function of T,S; :: thesis: for g being Function of S,V st rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds
(g * f) " = (f ") * (g ")
let g be Function of S,V; :: thesis: ( rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one implies (g * f) " = (f ") * (g ") )
assume that
A1: rng f = [#] S and
A2: f is one-to-one ; :: thesis: ( not dom g = [#] S or not rng g = [#] V or not g is one-to-one or (g * f) " = (f ") * (g ") )
assume that
A3: dom g = [#] S and
A4: rng g = [#] V and
A5: g is one-to-one ; :: thesis: (g * f) " = (f ") * (g ")
A6: ( f is onto & g is onto ) by A1, A4, FUNCT_2:def 3;
rng (g * f) = [#] V by A1, A3, A4, RELAT_1:28;
then g * f is onto by FUNCT_2:def 3;
then A7: (g * f) " = (g * f) " by A2, A5, Def4;
A8: f " = f " by A2, A6, Def4;
g " = g " by A5, A6, Def4;
hence (g * f) " = (f ") * (g ") by A2, A5, A8, A7, FUNCT_1:44; :: thesis: verum