:: deftheorem Def2 defines |. NFCONT_4:def 2 :
for n being Element of NAT
for Z being set
for f being PartFunc of Z,(REAL n)
for b₄ being PartFunc of Z,REAL holds
( b₄ = |.f.| iff ( dom b₄ = dom f & ( for x being set st x in dom b₄ holds
b₄ /. x = |.(f /. x).| ) ) );