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 3 not A is empty
reconsider f = the charact of A as non empty Function by A1;
set x = the Element of dom f;
reconsider y = f . the Element of dom f as non empty set by A2;
A3:
y in rng f
by FUNCT_1:def 3;
rng f c= PFuncs (( the carrier of A *), the carrier of A)
by FINSEQ_1:def 4;
then A4:
y is PartFunc of ( the carrier of A *), the carrier of A
by A3, PARTFUN1:47;
reconsider y = y as non empty Function ;
thus
not the carrier of A is empty
by A4; STRUCT_0:def 1 verum