let D be non empty set ; :: thesis:
let f be Function; :: thesis:
set X = D;
A1: dom <:<*f*>:> = dom f by FINSEQ_3:141;
assume A2: rng f = D ; :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in rng <:<*f*>:> ; :: thesis:
then consider y being object such that
A3: y in dom <:<*f*>:> and
A4: <:<*f*>:> . y = x by FUNCT_1:def 3;
reconsider fy = f . y as Element of D by A2, A1, A3, FUNCT_1:3;
A5: <*fy*> is Element of 1 -tuples_on D by FINSEQ_2:131;
<:<*f*>:> . y = <*(f . y)*> by A1, A3, FINSEQ_3:141;
hence x in 1 -tuples_on D by A4, A5; :: thesis:

end;

assume x in 1 -tuples_on D ; :: thesis:
then x is Tuple of 1,D by FINSEQ_2:131;
then consider d being Element of D such that
A6: x = <*d*> by FINSEQ_2:97;
consider y being object such that
A7: y in dom f and
A8: f . y = d by A2, FUNCT_1:def 3;
<:<*f*>:> . y = <*d*> by A7, A8, FINSEQ_3:141;
hence x in rng <:<*f*>:> by A1, A6, A7, FUNCT_1:3; :: thesis:

end;

hence rng <:<*f*>:> = 1 -tuples_on D by TARSKI:2; :: thesis: