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;
A1: dom <:<*f*>:> = dom f by FINSEQ_3:141;
assume A2: rng f = D ; :: thesis: rng <:<*f*>:> = 1 -tuples_on D

now :: thesis: for x being object holds
( ( x in rng <:<*f*>:> implies x in 1 -tuples_on D ) & ( x in 1 -tuples_on D implies x in rng <:<*f*>:> ) )

let x be object ; :: 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 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: verum

end;

assume x in 1 -tuples_on D ; :: thesis: x in rng <:<*f*>:>
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: verum

end;

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