let p1, p2, p3 be set ; :: thesis: ( p1 <> p2 implies p2 .. <*p1,p2,p3*> = 2 )
A2: <*p1,p2,p3*> . 1 = p1 ;
assume A3: p1 <> p2 ; :: thesis: p2 .. <*p1,p2,p3*> = 2

A4: now :: thesis: for i being Nat st 1 <= i & i < 1 + 1 holds
<*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2

let i be Nat; :: thesis: ( 1 <= i & i < 1 + 1 implies <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2 )
assume A5: 1 <= i ; :: thesis: ( i < 1 + 1 implies <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2 )
assume i < 1 + 1 ; :: thesis: <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2
then i <= 1 by NAT_1:13;
hence <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2 by A3, A2, A5, XXREAL_0:1; :: thesis: 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 A4, Th2; :: thesis: verum