set f = U -multiCat ;
set C = U * ;
set D = (U *) * ;

now

let x be set ; :: thesis: ( x in dom (U -multiCat) implies (U -multiCat) . x is FinSequence )
assume x in dom (U -multiCat) ; :: thesis: (U -multiCat) . x is FinSequence
then reconsider xx = x as Element of dom (U -multiCat) ;
(U -multiCat) . xx is Element of U * ;
hence (U -multiCat) . x is FinSequence ; :: thesis: verum

end;

hence for b₁ being Function st b₁ = U -multiCat holds
b₁ is FinSequence-yielding by PRE_POLY:def 3; :: thesis: verum