let b be BinOps 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 Def6;
b . xx is BinOp of (a . xx) by Def6;
hence b . x is Function ; :: thesis: verum