let p1, p2, p3 be set ; ( p1 <> p2 implies p2 .. <*p1,p2,p3*> = 2 )
A1:
<*p1,p2,p3*> . 2 = p2
by FINSEQ_1:45;
A2:
<*p1,p2,p3*> . 1 = p1
by FINSEQ_1:45;
assume A3:
p1 <> p2
; p2 .. <*p1,p2,p3*> = 2
A4:
now for i being Nat st 1 <= i & i < 1 + 1 holds
<*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2let i be
Nat;
( 1 <= i & i < 1 + 1 implies <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2 )assume A5:
1
<= i
;
( i < 1 + 1 implies <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2 )assume
i < 1
+ 1
;
<*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2then
i <= 1
by NAT_1:13;
hence
<*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2
by A3, A1, A2, A5, XXREAL_0:1;
verum end;
len <*p1,p2,p3*> = 3
by FINSEQ_1:45;
then
2 in dom <*p1,p2,p3*>
by FINSEQ_3:25;
hence
p2 .. <*p1,p2,p3*> = 2
by A1, A4, Th2; verum