theorem :: UNIALG_1:1

for n being Nat
for U1 being non empty partial non-empty UAStr st n in dom the charact of U1 holds
the charact of U1 . n is PartFunc of ( the carrier of U1 *), the carrier of U1 ;