let x1, x2, x3, x4, x5 be object ; 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 ;
( 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 ) )
( 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}
;
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
;
ex x being object st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )take
1
;
( 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;
y = <*x1,x2,x3,x4,x5*> . 1thus
y = <*x1,x2,x3,x4,x5*> . 1
by A3, FINSEQ_4:78;
verum end; suppose A4:
y = x2
;
ex x being object st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )take
2
;
( 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;
y = <*x1,x2,x3,x4,x5*> . 2thus
y = <*x1,x2,x3,x4,x5*> . 2
by A4, FINSEQ_4:78;
verum end; suppose A5:
y = x3
;
ex x being object st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )take
3
;
( 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;
y = <*x1,x2,x3,x4,x5*> . 3thus
y = <*x1,x2,x3,x4,x5*> . 3
by A5, FINSEQ_4:78;
verum end; suppose A6:
y = x4
;
ex x being object st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )take
4
;
( 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;
y = <*x1,x2,x3,x4,x5*> . 4thus
y = <*x1,x2,x3,x4,x5*> . 4
by A6, FINSEQ_4:78;
verum end; suppose A7:
y = x5
;
ex x being object st
( x in dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*> . x )take
5
;
( 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;
y = <*x1,x2,x3,x4,x5*> . 5thus
y = <*x1,x2,x3,x4,x5*> . 5
by A7, FINSEQ_4:78;
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
;
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 )
by FINSEQ_4:78;
hence
y in {x1,x2,x3,x4,x5}
by A9, ENUMSET1:def 3;
verum
end;
hence
rng <*x1,x2,x3,x4,x5*> = {x1,x2,x3,x4,x5}
by FUNCT_1:def 3; verum