set e = x SubstWith u;
for y being object st y in dom (x SubstWith u) holds
(x SubstWith u) . y is FinSequence ;
hence for b₁ being Function st b₁ = x SubstWith u holds
b₁ is FinSequence-yielding by PRE_POLY:def 3; :: thesis: verum