let x be Relation; :: thesis: ( x is primitive-recursive implies ( x is homogeneous & x is to-naturals & x is from-natural-fseqs ) )
assume x in PrimRec ; :: according to COMPUT_1:def 19 :: thesis: ( x is homogeneous & x is to-naturals & x is from-natural-fseqs )
then x is Element of PrimRec ;
hence ( x is homogeneous & x is to-naturals & x is from-natural-fseqs ) ; :: thesis: verum