let x1, x2, x3, x4 be object ; :: thesis:
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:
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:

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:

per cases by A2, ENUMSET1:def 2;

suppose A3: y = x1 ; :: thesis:

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

end;

suppose A4: y = x2 ; :: thesis:

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

end;

suppose A5: y = x3 ; :: thesis:

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

end;

suppose A6: y = x4 ; :: thesis:

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

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:
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 ) by FINSEQ_4:76;
hence y in {x1,x2,x3,x4} by A8, ENUMSET1:def 2; :: thesis:

end;

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