let U be non empty set ; :: thesis: for p being FinSequence
for q being U -valued FinSequence st p is U * -valued holds
(U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q
let p be FinSequence; :: thesis: for q being U -valued FinSequence st p is U * -valued holds
(U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q
let q be U -valued FinSequence; :: thesis: ( p is U * -valued implies (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q )
set C = U -multiCat ;
set g = U -concatenation ;
set G = MultPlace (U -concatenation);
reconsider qq = q as FinSequence of U by Lm1;

per cases ( p is empty or not p is empty ) ;

suppose p is empty ; :: thesis: ( p is U * -valued implies (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q )

then reconsider e = p as empty set ;
A1: ( ((U -multiCat) . e) ^ q = q & (U -multiCat) . (e ^ <*q*>) = (U -multiCat) . <*q*> ) ;
(U -multiCat) . (e ^ <*q*>) = (MultPlace (U -concatenation)) . <*qq*> by Th32
.= qq by Th31 ;
hence ( p is U * -valued implies (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q ) by A1; :: thesis: verum

end;

suppose A2: not p is empty ; :: thesis: ( p is U * -valued implies (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q )

assume p is U * -valued ; :: thesis: (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q
then reconsider pp = p as U * -valued non empty FinSequence by A2;
reconsider ppp = pp as non empty FinSequence of U * by Lm1;
(U -multiCat) . (pp ^ <*q*>) = (MultPlace (U -concatenation)) . (pp ^ <*qq*>) by Th32
.= (U -concatenation) . (((MultPlace (U -concatenation)) . pp),qq) by Th31
.= (U -concatenation) . (((U -multiCat) . ppp),q) by Th32
.= ((U -multiCat) . p) ^ q by Th4 ;
hence (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q ; :: thesis: verum

end;

end;