let x be NAT * -defined Function; :: thesis: ( x is primitive-recursive implies x is len-total )
assume x in PrimRec ; :: according to COMPUT_1:def 16 :: thesis: x is len-total
then x is Element of PrimRec ;
hence x is len-total ; :: thesis: verum