let x be object ; :: thesis: for f being Function st dom f = {x} holds
rng f = {(f . x)}
let f be Function; :: thesis: ( dom f = {x} implies rng f = {(f . x)} )
assume A1: dom f = {x} ; :: thesis: rng f = {(f . x)}
for y being object holds
( y in rng f iff y in {(f . x)} )
proof
let y be object ; :: thesis: ( y in rng f iff y in {(f . x)} )
thus ( y in rng f implies y in {(f . x)} ) :: thesis: ( y in {(f . x)} implies y in rng f )
proof
assume y in rng f ; :: thesis: y in {(f . x)}
then consider z being object such that
A2: z in dom f and
A3: y = f . z by Def3;
z = x by A1, A2, TARSKI:def 1;
hence y in {(f . x)} by A3, TARSKI:def 1; :: thesis: verum
end;
assume y in {(f . x)} ; :: thesis: y in rng f
then A4: y = f . x by TARSKI:def 1;
x in dom f by A1, TARSKI:def 1;
hence y in rng f by A4, Def3; :: thesis: verum
end;
hence rng f = {(f . x)} by TARSKI:2; :: thesis: verum