reconsider f = U -concatenation as BinOp of (U *) ;
q1 is FinSequence of U by Lm1;
then reconsider q11 = q1 as Element of U * ;
set F = MultPlace f;
set p = <*q11*>;
set C = U -multiCat ;
(U -multiCat) . <*q1,q2*> = ((U -multiCat) . <*q11*>) ^ q2 by Th33
.= ((MultPlace f) . <*q11*>) ^ q2 by Th32
.= q1 ^ q2 by Lm15 ;
hence for b₁ being set st b₁ = ((U -multiCat) . <*q1,q2*>) \+\ (q1 ^ q2) holds
b₁ is empty ; :: thesis: verum