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 Th76, TARSKI:def 4;
ex m being object st
( m in dom PrimRec-Approximation & PrimRec-Approximation . m = X ) by A2, FUNCT_1:def 3;
hence ( f is quasi_total & f is homogeneous ) by A1, Th77; :: thesis: verum