:: deftheorem defines \; AOFA_000:def 17 :
for A being non-empty with_catenation UAStr
for I1, I2 being Algorithm of A holds I1 \; I2 = (Den ((In (2,(dom the charact of A))),A)) . <*I1,I2*>;