let A be non-empty with_while-instruction UAStr ; :: thesis: dom (Den ((In (4,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A
reconsider f = the charact of A . 4 as non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of A *), the carrier of A by Def13;
4 in dom the charact of A by Def13;
then A1: Den ((In (4,(dom the charact of A))),A) = f by SUBSET_1:def 8;
arity f = 2 by COMPUT_1:def 21;
hence dom (Den ((In (4,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A by A1, COMPUT_1:22; :: thesis: verum