reconsider A = rng the charact of U0 as non empty set by RELAT_1:64;

now

let x be Element of A; :: thesis: x is non empty homogeneous quasi_total PartFunc of U0
consider i being Nat such that
A1: ( i in dom the charact of U0 & the charact of U0 . i = x ) by FINSEQ_2:11;
reconsider p = the charact of U0 . i as PartFunc of U0 by A1, UNIALG_1:5;
( p is homogeneous & p is quasi_total & not p is empty ) by A1, FUNCT_1:def 15, UNIALG_1:def 5;
hence x is non empty homogeneous quasi_total PartFunc of U0 by A1; :: thesis: verum

end;

hence rng the charact of U0 is PFuncsDomHQN of U0 by Def1; :: thesis: verum