let A be UAStr ; ( A is non-empty implies not A is empty )
assume that
A1:
the charact of A <> {}
and
A2:
the charact of A is non-empty
; UNIALG_1:def 9 not A is empty
reconsider f = the charact of A as non empty Function by A1;
consider x being Element of dom f;
reconsider y = f . x as non empty set by A2;
A3:
y in rng f
by FUNCT_1:def 5;
A4:
rng f c= PFuncs (the carrier of A * ),the carrier of A
by FINSEQ_1:def 4;
then A5:
y is PartFunc of (the carrier of A * ),the carrier of A
by A3, PARTFUN1:121;
reconsider y = y as non empty Function by A3, A4;
consider z being Element of rng y;
thus
not the carrier of A is empty
by A5; STRUCT_0:def 1 verum