:: by Yasuho Mizuhara and Takaya Nishiyama

::

:: Received March 18, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

Lm1: for n being Nat

for p, q being Tuple of n, BOOLEAN st len p = n & len q = n & ( for i being Nat st i in Seg n holds

p /. i = q /. i ) holds

p = q

proof end;