theorem Th47: :: AOFA_000:47

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