theorem Th3: :: NOMIN_9:3

for a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 being object
for f being FinSequence holds
( f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> iff ( len f = 10 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 & f . 7 = a7 & f . 8 = a8 & f . 9 = a9 & f . 10 = a10 ) )