let p1,

p2 be

set ;

p1 .. <*p1,p2*> = 1
A1:
for i being Nat st 1

<= i &

i < 1 holds

<*p1,p2*> . i <> <*p1,p2*> . 1
;

len <*p1,p2*> = 2

by FINSEQ_1:44;

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

<*p1,p2*> . 1

= p1
by FINSEQ_1:44;

hence
p1 .. <*p1,p2*> = 1

by A2, A1, Th2;

verum