let X be set ; :: thesis: for C being non empty set holds chi X,C is total
let C be non empty set ; :: thesis: chi X,C is total
dom (chi X,C) = C by Th77;
hence chi X,C is total by PARTFUN1:def 4; :: thesis: verum