set prd = PrimRec-Approximation ;
let f be Element of PrimRec ; :: thesis: ( f is quasi_total & f is homogeneous )
consider X being set such that
A1: f in X and
A2: X in rng PrimRec-Approximation by Th81, TARSKI:def 4;
ex m being set st
( m in dom PrimRec-Approximation & PrimRec-Approximation . m = X ) by A2, FUNCT_1:def 5;
hence ( f is quasi_total & f is homogeneous ) by A1, Th82; :: thesis: verum