set f = U -multiCat ;
set C = U * ;
set D = (U *) * ;
for x being object st x in dom (U -multiCat) holds
(U -multiCat) . x is FinSequence ;
hence for b₁ being Function st b₁ = U -multiCat holds
b₁ is FinSequence-yielding by PRE_POLY:def 3; :: thesis: verum