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

proof

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

proof

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

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

given x being object such that A7: x in dom <*x1,x2,x3,x4*> and
A8: y = <*x1,x2,x3,x4*> . x ; :: thesis: y in {x1,x2,x3,x4}
x in Seg 4 by A7, FINSEQ_1:89;
then ( x = 1 or x = 2 or x = 3 or x = 4 ) by ENUMSET1:def 2, FINSEQ_3:2;
then ( <*x1,x2,x3,x4*> . x = x1 or <*x1,x2,x3,x4*> . x = x2 or <*x1,x2,x3,x4*> . x = x3 or <*x1,x2,x3,x4*> . x = x4 ) ;
hence y in {x1,x2,x3,x4} by A8, ENUMSET1:def 2; :: thesis: verum

end;

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