let T be 1-sorted ; :: thesis: for S being non empty 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
(f ") " = f
let S be non empty 1-sorted ; :: thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds
(f ") " = f
let f be Function of T,S; :: thesis: ( rng f = [#] S & f is one-to-one implies (f ") " = f )
assume that
A1: rng f = [#] S and
A2: f is one-to-one ; :: thesis: (f ") " = f
A3: f is onto by A1, FUNCT_2:def 3;
f = (f ") " by A2, FUNCT_1:43;
then A4: f = (f ") " by A3, A2, Def4;
A5: f " is one-to-one by A1, A2, Th50;
rng (f ") = [#] T by A1, A2, Th49;
then f " is onto by FUNCT_2:def 3;
hence (f ") " = f by A4, A5, Def4; :: thesis: verum