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

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 and
A2: the charact of U0 . i = x by FINSEQ_2:10;
reconsider p = the charact of U0 . i as PartFunc of U0 by A1, UNIALG_1:1;
( p is homogeneous & p is quasi_total & not p is empty ) by A1, FUNCT_1:def 9, MARGREL1:def 24;
hence x is non empty homogeneous quasi_total PartFunc of U0 by A2; :: thesis: verum

end;

hence rng the charact of U0 is PFuncsDomHQN of U0 by MARGREL1:def 26; :: thesis: verum