for A being non-empty with_empty-instruction UAStr holds dom (Den ((In (1,(dom the charact of A))),A)) = {{}}