let p1, p2, p3 be set ; <*p1,p2,p3*> | (Seg 1) = <*p1*>
set f = <*p1,p2,p3*> | (Seg 1);
len <*p1,p2,p3*> = 3
by FINSEQ_1:45;
then
1 in dom <*p1,p2,p3*>
by FINSEQ_3:25;
then A1:
Seg 1 c= dom <*p1,p2,p3*>
by FINSEQ_1:2, ZFMISC_1:31;
A2: dom (<*p1,p2,p3*> | (Seg 1)) =
(dom <*p1,p2,p3*>) /\ (Seg 1)
by RELAT_1:61
.=
Seg 1
by A1, XBOOLE_1:28
;
then reconsider f = <*p1,p2,p3*> | (Seg 1) as FinSequence by FINSEQ_1:def 2;
1 in dom f
by A2;
then A3: f . 1 =
<*p1,p2,p3*> . 1
by FUNCT_1:47
.=
p1
by FINSEQ_1:45
;
len f = 1
by A2, FINSEQ_1:def 3;
hence
<*p1,p2,p3*> | (Seg 1) = <*p1*>
by A3, FINSEQ_1:40; verum