let b be UnOps of a; :: thesis: b is Function-yielding
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom b or b . x is set )
assume x in dom b ; :: thesis: b . x is set
then reconsider xx = x as Element of dom a by Def7;
b . xx is UnOp of (a . xx) by Def7;
hence b . x is Function ; :: thesis: verum