let Y be set ; :: thesis: for U being non empty set
for p being FinSequence st p <> {} & p is Y -valued & Y c= U * & Y is with_non-empty_elements holds
(U -multiCat) . p <> {}
let U be non empty set ; :: thesis: for p being FinSequence st p <> {} & p is Y -valued & Y c= U * & Y is with_non-empty_elements holds
(U -multiCat) . p <> {}
let p be FinSequence; :: thesis: ( p <> {} & p is Y -valued & Y c= U * & Y is with_non-empty_elements implies (U -multiCat) . p <> {} )
assume p <> {} ; :: thesis: ( not p is Y -valued or not Y c= U * or not Y is with_non-empty_elements or (U -multiCat) . p <> {} )
then reconsider pp = p as non empty FinSequence ;
assume B0: ( p is Y -valued & Y c= U * & Y is with_non-empty_elements ) ; :: thesis: (U -multiCat) . p <> {}
then ( rng pp c= Y & Y c= U * ) by RELAT_1:def 19;
then reconsider YY = Y as non empty with_non-empty_elements Subset of (U *) by B0;
reconsider pp = pp as YY -valued non empty FinSequence by B0;
( pp is U * -valued & not pp is {} * -valued ) ;
hence (U -multiCat) . p <> {} by Th52; :: thesis: verum