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
A1: m + 1 = len W by NAT_1:6;
reconsider WW = W as (m + 1) + 0 -element FinSequence by A1, CARD_1:def 7;
A2: {(WW . (m + 1))} \ (((AllSymbolsOf S) *) \ {{}}) = {} ;
then A3: WW . (m + 1) in ((AllSymbolsOf S) *) \ {{}} by ZFMISC_1:60;
reconsider last = WW . (m + 1) as string of S by A2, ZFMISC_1:60;
reconsider lastt = WW . (m + 1) as Element of (AllSymbolsOf S) * by A3;
set VV = WW | (Seg m);
reconsider VVV = WW | (Seg m) as (AllSymbolsOf S) * -valued FinSequence ;
((WW | (Seg m)) ^ <*(WW . (m + 1))*>) \+\ WW = {} ;
then A4: (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 b1 being set st b1 = (S -multiCat) . W holds
not b1 is empty
then (MultPlace ((AllSymbolsOf S) -concatenation)) . W = (MultPlace ((AllSymbolsOf S) -concatenation)) . <*lastt*> by A4, FINSEQ_1:34
.= last by FOMODEL0:31 ;
hence for b1 being set st b1 = (S -multiCat) . W holds
not b1 is empty by FOMODEL0:32; :: thesis: verum
end;
suppose A5: not VVV is empty ; :: thesis: for b1 being set st b1 = (S -multiCat) . W holds
not b1 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 A5, A4, FOMODEL0:31
.= ((MultPlace ((AllSymbolsOf S) -concatenation)) . VVVV) ^ last by FOMODEL0:4 ;
hence for b1 being set st b1 = (S -multiCat) . W holds
not b1 is empty by FOMODEL0:32; :: thesis: verum
end;
end;