ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & rng p c= underlay S ) by Th16;
hence o `2 is FinSequence-like by MCART_1:7; :: thesis: verum