let x, X be set ; :: thesis: for U being non empty set st ex p being FinSequence st
( x = p & p is X * -valued ) holds
(U -multiCat) . x is X -valued
let U be non empty set ; :: thesis: ( ex p being FinSequence st
( x = p & p is X * -valued ) implies (U -multiCat) . x is X -valued )
set C = U -multiCat ;
B1: dom (U -multiCat) = (U *) * by FUNCT_2:def 1;
given p being FinSequence such that B0: ( x = p & p is X * -valued ) ; :: thesis: (U -multiCat) . x is X -valued
x is FinSequence of X * by B0, Lm45;
then reconsider px = x as Element of (X *) * by FINSEQ_1:def 11;

per cases ( (U -multiCat) . p <> {} or (U -multiCat) . p = {} ) ;

suppose C1: (U -multiCat) . p <> {} ; :: thesis: (U -multiCat) . x is X -valued

then ( p in (U *) * & p <> {} ) by B1, FUNCT_1:def 2;
then reconsider pp = x as non empty FinSequence of U * by Lm45, B0;
C0: ( pp is X * -valued & not pp is {} * -valued ) by Th52, B0, C1;
reconsider XX = X as non empty set by Th52, B0, C1;
set CX = XX -multiCat ;
reconsider pxx = px as Element of (XX *) * ;
(XX -multiCat) . pp <> {} by Th52, C0;
hence (U -multiCat) . x is X -valued by Th52, C1, B0; :: thesis: verum

end;

suppose (U -multiCat) . p = {} ; :: thesis: (U -multiCat) . x is X -valued

then reconsider e = (U -multiCat) . p as empty set ;
rng e c= X by XBOOLE_1:2;
hence (U -multiCat) . x is X -valued by B0, RELAT_1:def 19; :: thesis: verum

end;

end;