let Y be set ; :: thesis: for U1, U2 being non empty set
for p being FinSequence st U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements holds
(U1 -multiCat) . p = (U2 -multiCat) . p
let U1, U2 be non empty set ; :: thesis: for p being FinSequence st U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements holds
(U1 -multiCat) . p = (U2 -multiCat) . p
let p be FinSequence; :: thesis: ( U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements implies (U1 -multiCat) . p = (U2 -multiCat) . p )
assume U1 c= U2 ; :: thesis: ( not Y c= U1 * or not p is Y -valued or not p <> {} or not Y is with_non-empty_elements or (U1 -multiCat) . p = (U2 -multiCat) . p )
then reconsider U11 = U1 as non empty Subset of U2 ;
assume Y c= U1 * ; :: thesis: ( not p is Y -valued or not p <> {} or not Y is with_non-empty_elements or (U1 -multiCat) . p = (U2 -multiCat) . p )
then reconsider Y1 = Y as Subset of (U11 *) ;
reconsider Y2 = Y1 as Subset of (U2 *) by XBOOLE_1:1;
assume p is Y -valued ; :: thesis: ( not p <> {} or not Y is with_non-empty_elements or (U1 -multiCat) . p = (U2 -multiCat) . p )
then reconsider p1 = p as Y1 -valued FinSequence ;
reconsider p2 = p1 as Y2 -valued FinSequence ;
assume ( p <> {} & Y is with_non-empty_elements ) ; :: thesis: (U1 -multiCat) . p = (U2 -multiCat) . p
then ( (U1 -multiCat) . p1 <> {} & (U2 -multiCat) . p2 <> {} ) by Lm52;
hence (U1 -multiCat) . p = (U2 -multiCat) . p by Th52; :: thesis: verum