let p1, p3, p2 be set ; :: thesis: ( p1 <> p3 & p2 <> p3 implies p3 .. <*p1,p2,p3*> = 3 )
assume that
A1: p1 <> p3 and
A2: p2 <> p3 ; :: thesis: p3 .. <*p1,p2,p3*> = 3
A3: <*p1,p2,p3*> . 3 = p3 by FINSEQ_1:45;
A4: <*p1,p2,p3*> . 1 = p1 by FINSEQ_1:45;
A5: <*p1,p2,p3*> . 2 = p2 by FINSEQ_1:45;

A6: now

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

end;

3 <= len <*p1,p2,p3*> by FINSEQ_1:45;
then 3 in dom <*p1,p2,p3*> by FINSEQ_3:25;
hence p3 .. <*p1,p2,p3*> = 3 by A3, A6, Th4; :: thesis: verum