theorem :: FINSEQ_2:95

for i being natural Number
for D being non empty set
for z being Tuple of 0 ,D
for t being Tuple of i,D holds
( z ^ t = t & t ^ z = t ) by FINSEQ_1:34;