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