let x1, x2, x3, x4, x5 be set ; :: thesis: rng <*x1,x2,x3,x4,x5*> = {x1,x2,x3,x4,x5}
for y being set holds
( y in {x1,x2,x3,x4,x5} iff ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x ) )

proof

let y be set ; :: thesis: ( y in {x1,x2,x3,x4,x5} iff ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x ) )
thus ( y in {x1,x2,x3,x4,x5} implies ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x ) ) :: thesis: ( ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x ) implies y in {x1,x2,x3,x4,x5} )

proof

A1: dom <*x1,x2,x3,x4,x5*> = {1,2,3,4,5} by FINSEQ_3:3, FINSEQ_4:94;
assume A2: y in {x1,x2,x3,x4,x5} ; :: thesis: ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )

per cases ( y = x1 or y = x2 or y = x3 or y = x4 or y = x5 ) by A2, ENUMSET1:def 3;

suppose A3: y = x1 ; :: thesis: ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )

take 1 ; :: thesis: ( 1 in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . 1 )
thus 1 in dom <*x1,x2,x3,x4,x5*> by A1, ENUMSET1:def 3; :: thesis: y = <*x1,x2,x3,x4,x5*> . 1
thus y = <*x1,x2,x3,x4,x5*> . 1 by A3, FINSEQ_4:93; :: thesis: verum

end;

suppose A4: y = x2 ; :: thesis: ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )

take 2 ; :: thesis: ( 2 in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . 2 )
thus 2 in dom <*x1,x2,x3,x4,x5*> by A1, ENUMSET1:def 3; :: thesis: y = <*x1,x2,x3,x4,x5*> . 2
thus y = <*x1,x2,x3,x4,x5*> . 2 by A4, FINSEQ_4:93; :: thesis: verum

end;

suppose A5: y = x3 ; :: thesis: ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )

take 3 ; :: thesis: ( 3 in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . 3 )
thus 3 in dom <*x1,x2,x3,x4,x5*> by A1, ENUMSET1:def 3; :: thesis: y = <*x1,x2,x3,x4,x5*> . 3
thus y = <*x1,x2,x3,x4,x5*> . 3 by A5, FINSEQ_4:93; :: thesis: verum

end;

suppose A6: y = x4 ; :: thesis: ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )

take 4 ; :: thesis: ( 4 in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . 4 )
thus 4 in dom <*x1,x2,x3,x4,x5*> by A1, ENUMSET1:def 3; :: thesis: y = <*x1,x2,x3,x4,x5*> . 4
thus y = <*x1,x2,x3,x4,x5*> . 4 by A6, FINSEQ_4:93; :: thesis: verum

end;

suppose A7: y = x5 ; :: thesis: ex x being set st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )

take 5 ; :: thesis: ( 5 in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . 5 )
thus 5 in dom <*x1,x2,x3,x4,x5*> by A1, ENUMSET1:def 3; :: thesis: y = <*x1,x2,x3,x4,x5*> . 5
thus y = <*x1,x2,x3,x4,x5*> . 5 by A7, FINSEQ_4:93; :: thesis: verum

end;

end;

end;

given x being set such that A8: ( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x ) ; :: thesis: y in {x1,x2,x3,x4,x5}
x in Seg 5 by A8, FINSEQ_4:94;
then ( x = 1 or x = 2 or x = 3 or x = 4 or x = 5 ) by ENUMSET1:def 3, FINSEQ_3:3;
then ( <*x1,x2,x3,x4,x5*> . x = x1 or <*x1,x2,x3,x4,x5*> . x = x2 or <*x1,x2,x3,x4,x5*> . x = x3 or <*x1,x2,x3,x4,x5*> . x = x4 or <*x1,x2,x3,x4,x5*> . x = x5 ) by FINSEQ_4:93;
hence y in {x1,x2,x3,x4,x5} by A8, ENUMSET1:def 3; :: thesis: verum

end;

hence rng <*x1,x2,x3,x4,x5*> = {x1,x2,x3,x4,x5} by FUNCT_1:def 5; :: thesis: verum