theorem Th48: :: AOFA_000:48

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