let D be non empty set ; :: thesis: for f being Function st rng f = D holds
rng <:<*f*>:> = 1 -tuples_on D
let f be Function; :: thesis: ( rng f = D implies rng <:<*f*>:> = 1 -tuples_on D )
set X = D;
assume A1: rng f = D ; :: thesis: rng <:<*f*>:> = 1 -tuples_on D
A2: dom <:<*f*>:> = dom f by FUNCT_6:61;

now

let x be set ; :: thesis: ( ( x in rng <:<*f*>:> implies x in 1 -tuples_on D ) & ( x in 1 -tuples_on D implies x in rng <:<*f*>:> ) )

hereby :: thesis: ( x in 1 -tuples_on D implies x in rng <:<*f*>:> )

assume x in rng <:<*f*>:> ; :: thesis: x in 1 -tuples_on D
then consider y being set such that
A3: ( y in dom <:<*f*>:> & <:<*f*>:> . y = x ) by FUNCT_1:def 5;
A4: <:<*f*>:> . y = <*(f . y)*> by A2, A3, FUNCT_6:61;
reconsider fy = f . y as Element of D by A1, A2, A3, FUNCT_1:12;
<*fy*> is Element of 1 -tuples_on D ;
hence x in 1 -tuples_on D by A3, A4; :: thesis: verum

end;

assume x in 1 -tuples_on D ; :: thesis: x in rng <:<*f*>:>
then consider d being Element of D such that
A5: x = <*d*> by FINSEQ_2:117;
consider y being set such that
A6: ( y in dom f & f . y = d ) by A1, FUNCT_1:def 5;
<:<*f*>:> . y = <*d*> by A6, FUNCT_6:61;
hence x in rng <:<*f*>:> by A2, A5, A6, FUNCT_1:12; :: thesis: verum

end;

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