ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & rng p c= underlay S ) by Th7;
hence for b₁ being Function st b₁ = o `2 holds
b₁ is FinSequence-like ; :: thesis: verum