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

A4: now

let i be Nat; :: thesis: ( 1 <= i & i < 1 + 1 implies <*p1,p2*> . i <> <*p1,p2*> . 2 )
assume A5: 1 <= i ; :: thesis: ( i < 1 + 1 implies <*p1,p2*> . i <> <*p1,p2*> . 2 )
assume i < 1 + 1 ; :: thesis: <*p1,p2*> . i <> <*p1,p2*> . 2
then i <= 1 by NAT_1:13;
hence <*p1,p2*> . i <> <*p1,p2*> . 2 by A3, A1, A2, A5, XXREAL_0:1; :: thesis: verum

end;

2 <= len <*p1,p2*> by FINSEQ_1:44;
then 2 in dom <*p1,p2*> by FINSEQ_3:25;
hence p2 .. <*p1,p2*> = 2 by A1, A4, Th4; :: thesis: verum