rng <*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*> c= D
proof
let x be
object ;
TARSKI:def 3 ( not x in rng <*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*> or x in D )
assume
x in rng <*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*>
;
x in D
then
x in {((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)}
by FINSEQ_2:128;
then A2:
(
x = (p . 1) . 1 or
x = (p . 2) . 1 or
x = (p . 3) . 1 )
by ENUMSET1:def 1;
A3:
dom p = Seg 3
by A1, FINSEQ_1:def 3;
then A4:
p . 1
in rng p
by FINSEQ_1:1, FUNCT_1:3;
A5:
rng p c= 1
-tuples_on D
by FINSEQ_1:def 4;
A0:
1
-tuples_on D = { <*d*> where d is Element of D : verum }
by FINSEQ_2:96;
then
p . 1
in { <*d*> where d is Element of D : verum }
by A4, A5;
then consider d being
Element of
D such that A6:
p . 1
= <*d*>
;
A7:
(p . 1) . 1
= d
by A6, FINSEQ_1:def 8;
p . 2
in rng p
by A3, FINSEQ_1:1, FUNCT_1:3;
then
p . 2
in { <*d*> where d is Element of D : verum }
by A0, A5;
then consider d being
Element of
D such that A10:
p . 2
= <*d*>
;
A11:
(p . 2) . 1
= d
by A10, FINSEQ_1:def 8;
A12:
p . 3
in rng p
by A3, FINSEQ_1:1, FUNCT_1:3;
p . 3
in 1
-tuples_on D
by A5, A12;
then consider d being
Element of
D such that A14:
p . 3
= <*d*>
by A0;
(p . 3) . 1
= d
by A14, FINSEQ_1:def 8;
hence
x in D
by A2, A7, A11;
verum
end;
hence
<*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*> is FinSequence of D
by FINSEQ_1:def 4; verum