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

proof

let y be object ; :: thesis: ( y in {x1,x2,x3,x4,x5} iff ex x being object 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 object st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x ) ) :: thesis: ( ex x being object 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_1:89, FINSEQ_3:3;
assume A2: y in {x1,x2,x3,x4,x5} ; :: thesis: ex x being object 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 object 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; :: thesis: verum

end;

suppose A4: y = x2 ; :: thesis: ex x being object 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; :: thesis: verum

end;

suppose A5: y = x3 ; :: thesis: ex x being object 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; :: thesis: verum

end;

suppose A6: y = x4 ; :: thesis: ex x being object 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; :: thesis: verum

end;

suppose A7: y = x5 ; :: thesis: ex x being object 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; :: thesis: verum

end;

end;

end;

given x being object such that A8: x in dom <*x1,x2,x3,x4,x5*> and
A9: y = <*x1,x2,x3,x4,x5*> . x ; :: thesis: y in {x1,x2,x3,x4,x5}
x in Seg 5 by A8, FINSEQ_1:89;
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 ) ;
hence y in {x1,x2,x3,x4,x5} by A9, ENUMSET1:def 3; :: thesis: verum

end;

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