let X be non empty set ; :: thesis: for Z being set
for r being Renaming of X,Z holds r " is onto
let Z be set ; :: thesis: for r being Renaming of X,Z holds r " is onto
let r be Renaming of X,Z; :: thesis: r " is onto

A: now :: thesis: for o being object st o in X holds
o in rng (r ")

let o be object ; :: thesis: ( o in X implies o in rng (r ") )
assume o in X ; :: thesis: o in rng (r ")
then H: o in dom r by defr;
then r . o in rng r by FUNCT_1:3;
then r . o in dom (r ") by FUNCT_2:def 1;
then (r ") . (r . o) in rng (r ") by FUNCT_1:3;
hence o in rng (r ") by H, FUNCT_1:34; :: thesis: verum

end;

now :: thesis: for o being object st o in rng (r ") holds
o in X

let o be object ; :: thesis: ( o in rng (r ") implies o in X )
assume o in rng (r ") ; :: thesis: o in X
then o in dom r by FUNCT_1:33;
hence o in X ; :: thesis: verum

end;

hence r " is onto by A, TARSKI:2; :: thesis: verum