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