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:111 ; :: thesis: verum