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

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

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, 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 A4, Th2; :: thesis: verum