let m, n1, n2 be Nat; :: thesis: ( 1 <= n1 & n1 <= m & 1 <= n2 & n2 <= m & m proj n1 = m proj n2 implies n1 = n2 )
assume that
A1: ( 1 <= n1 & n1 <= m ) and
A2: ( 1 <= n2 & n2 <= m ) and
A3: m proj n1 = m proj n2 ; :: thesis: n1 = n2
set x = idseq m;
idseq m is Element of m -tuples_on NAT by FINSEQ_2:111;
then A4: ( (m proj n1) . (idseq m) = (idseq m) . n1 & (m proj n2) . (idseq m) = (idseq m) . n2 ) by COMPUT_1:38;
n1 in Seg m by A1, FINSEQ_1:1;
then A5: (idseq m) . n1 = n1 by FINSEQ_2:49;
n2 in Seg m by A2, FINSEQ_1:1;
hence n1 = n2 by A3, A4, A5, FINSEQ_2:49; :: thesis: verum