set C = S -multiCat ;
set SS = AllSymbolsOf S;
set g = (AllSymbolsOf S) -concatenation ;
set G = MultPlace ((AllSymbolsOf S) -concatenation);
consider m being Nat such that
B0: m + 1 = len W by NAT_1:6;
reconsider WW = W as (m + 1) + 0 -element FinSequence by B0, CARD_1:def 7;
Z0: {(WW . (m + 1))} \ (((AllSymbolsOf S) *) \ {{}}) = {} ;
then B1: WW . (m + 1) in ((AllSymbolsOf S) *) \ {{}} by ZFMISC_1:60;
reconsider last = WW . (m + 1) as string of S by Z0, ZFMISC_1:60;
reconsider lastt = WW . (m + 1) as Element of (AllSymbolsOf S) * by B1;
set VV = WW | (Seg m);
reconsider VVV = WW | (Seg m) as (AllSymbolsOf S) * -valued FinSequence ;
((WW | (Seg m)) ^ <*(WW . (m + 1))*>) \+\ WW = {} ;
then B2: (MultPlace ((AllSymbolsOf S) -concatenation)) . W = (MultPlace ((AllSymbolsOf S) -concatenation)) . (VVV ^ <*lastt*>) by FOMODEL0:29;

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

suppose VVV is empty ; :: thesis: for b₁ being set st b₁ = (S -multiCat) . W holds
not b₁ is empty

then (MultPlace ((AllSymbolsOf S) -concatenation)) . W = (MultPlace ((AllSymbolsOf S) -concatenation)) . <*lastt*> by B2, FINSEQ_1:34
.= last by FOMODEL0:31 ;
hence for b₁ being set st b₁ = (S -multiCat) . W holds
not b₁ is empty by FOMODEL0:32; :: thesis: verum

end;

suppose C0: not VVV is empty ; :: thesis: for b₁ being set st b₁ = (S -multiCat) . W holds
not b₁ is empty

then reconsider VVVV = VVV as Element of (((AllSymbolsOf S) *) *) \ {{}} by FOMODEL0:30;
(MultPlace ((AllSymbolsOf S) -concatenation)) . W = ((AllSymbolsOf S) -concatenation) . (((MultPlace ((AllSymbolsOf S) -concatenation)) . VVV),lastt) by C0, B2, FOMODEL0:31
.= ((MultPlace ((AllSymbolsOf S) -concatenation)) . VVVV) ^ last by FOMODEL0:4 ;
hence for b₁ being set st b₁ = (S -multiCat) . W holds
not b₁ is empty by FOMODEL0:32; :: thesis: verum

end;

end;