:: deftheorem Def7 defines UnOps PRVECT_1:def 7 :
for a being non-empty non empty Function
for b₂ being Function holds
( b₂ is UnOps of a iff ( dom b₂ = dom a & ( for i being Element of dom a holds b₂ . i is UnOp of (a . i) ) ) );