let p1, p2, p3 be set ; :: thesis: p1 .. <*p1,p2,p3*> = 1
len <*p1,p2,p3*> = 3 by FINSEQ_1:62;
then A1: 1 in dom <*p1,p2,p3*> by FINSEQ_3:27;
A2: <*p1,p2,p3*> . 1 = p1 by FINSEQ_1:62;
for i being Nat st 1 <= i & i < 1 holds
<*p1,p2,p3*> . i <> <*p1,p2,p3*> . 1 ;
hence p1 .. <*p1,p2,p3*> = 1 by A1, A2, Th4; :: thesis: verum