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

now :: thesis: for x being Element of A holds x is non empty homogeneous quasi_total PartFunc of U0

hence
rng the charact of U0 is PFuncsDomHQN of U0
by MARGREL1:def 26; :: thesis: verumlet 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 ;

( 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;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 ;

( 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