theorem Th44: :: AOFA_000:44

for A being non-empty with_catenation UAStr holds dom (Den ((In (2,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A