let D be non empty set ; :: thesis: for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = Funcs ((Seg (arity h)),D)
let h be non empty homogeneous quasi_total PartFunc of (D *),D; :: thesis: dom h = Funcs ((Seg (arity h)),D)
thus dom h = (arity h) -tuples_on D by Lm1
.= Funcs ((Seg (arity h)),D) by FINSEQ_2:93 ; :: thesis: verum