let X be set ; :: thesis: for F being BinOp of X
for A being b₁ -binopclosed Subset of X holds F || A is BinOp of A
let F be BinOp of X; :: thesis: for A being F -binopclosed Subset of X holds F || A is BinOp of A
let A be F -binopclosed Subset of X; :: thesis: F || A is BinOp of A
dom F = [:X,X:] by PARTFUN1:def 2;
then A1: dom (F || A) = [:A,A:] by RELAT_1:62, ZFMISC_1:96;
for x being object st x in [:A,A:] holds
(F || A) . x in A

proof

let x be object ; :: thesis: ( x in [:A,A:] implies (F || A) . x in A )
assume A2: x in [:A,A:] ; :: thesis: (F || A) . x in A
then (F || A) . x = F . x by A1, FUNCT_1:47;
hence (F || A) . x in A by A2, Def1; :: thesis: verum

end;

hence F || A is BinOp of A by A1, FUNCT_2:3; :: thesis: verum