:: deftheorem Def11 defines with_catenation AOFA_000:def 11 :
for S being non empty UAStr holds
( S is with_catenation iff ( 2 in dom the charact of S & the charact of S . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S ) );