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