let p1, p2, p3 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

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

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;
then not not i = 0 & ... & not i = 2 ;
hence <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 3 by A1, A2, A7; :: 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 A6, Th2; :: thesis: verum