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 Relation-like & o `2 is Function-like ) by MCART_1:7; :: thesis: verum