let E be non empty set ; :: thesis: for f being Function st dom f = E & ( for d being Element of E holds f . d = f .: d ) holds
rng f is epsilon-transitive
let f be Function; :: thesis: ( dom f = E & ( for d being Element of E holds f . d = f .: d ) implies rng f is epsilon-transitive )
assume A1: ( dom f = E & ( for d being Element of E holds f . d = f .: d ) ) ; :: thesis: rng f is epsilon-transitive
let Y be set ; :: according to ORDINAL1:def 2 :: thesis: ( not Y in rng f or Y c= rng f )
assume A2: Y in rng f ; :: thesis: Y c= rng f
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in rng f )
assume A3: a in Y ; :: thesis: a in rng f
consider b being set such that
A4: ( b in dom f & Y = f . b ) by A2, FUNCT_1:def 5;
reconsider d = b as Element of E by A1, A4;
f . d = f .: d by A1;
then ex c being set st
( c in dom f & c in d & a = f . c ) by A3, A4, FUNCT_1:def 12;
hence a in rng f by FUNCT_1:def 5; :: thesis: verum