let p1, p2 be set ; :: thesis: <*p1,p2*> | (Seg 1) = <*p1*>

set f = <*p1,p2*> | (Seg 1);

len <*p1,p2*> = 2 by FINSEQ_1:44;

then 1 in dom <*p1,p2*> by FINSEQ_3:25;

then A1: Seg 1 c= dom <*p1,p2*> by FINSEQ_1:2, ZFMISC_1:31;

A2: dom (<*p1,p2*> | (Seg 1)) = (dom <*p1,p2*>) /\ (Seg 1) by RELAT_1:61

.= Seg 1 by A1, XBOOLE_1:28 ;

then reconsider f = <*p1,p2*> | (Seg 1) as FinSequence by FINSEQ_1:def 2;

1 in dom f by A2;

then A3: f . 1 = <*p1,p2*> . 1 by FUNCT_1:47

.= p1 by FINSEQ_1:44 ;

len f = 1 by A2, FINSEQ_1:def 3;

hence <*p1,p2*> | (Seg 1) = <*p1*> by A3, FINSEQ_1:40; :: thesis: verum

set f = <*p1,p2*> | (Seg 1);

len <*p1,p2*> = 2 by FINSEQ_1:44;

then 1 in dom <*p1,p2*> by FINSEQ_3:25;

then A1: Seg 1 c= dom <*p1,p2*> by FINSEQ_1:2, ZFMISC_1:31;

A2: dom (<*p1,p2*> | (Seg 1)) = (dom <*p1,p2*>) /\ (Seg 1) by RELAT_1:61

.= Seg 1 by A1, XBOOLE_1:28 ;

then reconsider f = <*p1,p2*> | (Seg 1) as FinSequence by FINSEQ_1:def 2;

1 in dom f by A2;

then A3: f . 1 = <*p1,p2*> . 1 by FUNCT_1:47

.= p1 by FINSEQ_1:44 ;

len f = 1 by A2, FINSEQ_1:def 3;

hence <*p1,p2*> | (Seg 1) = <*p1*> by A3, FINSEQ_1:40; :: thesis: verum