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

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