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 that
A1: dom f = E and
A2: 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 Y in rng f ; :: thesis: Y c= rng f
then consider b being object such that
A3: b in dom f and
A4: Y = f . b by FUNCT_1:def 3;
reconsider d = b as Element of E by A1, A3;
A5: f . d = f .: d by A2;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in rng f )
assume a in Y ; :: thesis: a in rng f
then ex c being object st
( c in dom f & c in d & a = f . c ) by A4, A5, FUNCT_1:def 6;
hence a in rng f by FUNCT_1:def 3; :: thesis: verum