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

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 ")

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;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

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

o in X

hence
r " is onto
by A, TARSKI:2; :: thesis: verumo 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;assume o in rng (r ") ; :: thesis: o in X

then o in dom r by FUNCT_1:33;

hence o in X ; :: thesis: verum