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 ;
A1: dom (U -multiCat) = (U *) * by FUNCT_2:def 1;
given p being FinSequence such that A2: ( x = p & p is X * -valued ) ; :: thesis: (U -multiCat) . x is X -valued
x is FinSequence of X * by A2, Lm1;
then reconsider px = x as Element of (X *) * ;

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

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

then ( p in (U *) * & p <> {} ) by FUNCT_1:def 2, A1;
then reconsider pp = x as non empty FinSequence of U * by Lm1, A2;
A4: ( pp is X * -valued & not pp is {} * -valued ) by Th52, A2, A3;
reconsider XX = X as non empty set by Th52, A2, A3;
set CX = XX -multiCat ;
reconsider pxx = px as Element of (XX *) * ;
(XX -multiCat) . pp <> {} by Th52, A4;
hence (U -multiCat) . x is X -valued by Th52, A3, A2; :: 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 ;
hence (U -multiCat) . x is X -valued by A2; :: thesis: verum

end;

end;