let X be set ; :: thesis: for A being Subset of X
for F being Presv of X,A holds F || A is BinOp of A
let A be Subset of X; :: thesis: for F being Presv of X,A holds F || A is BinOp of A
let F be Presv of X,A; :: thesis: F || A is BinOp of A
( X = {} implies [:X,X:] = {} ) ;
then dom F = [:X,X:] by FUNCT_2:def 1;
then A1: dom (F || A) = [:A,A:] by RELAT_1:62, ZFMISC_1:96;
for x being set st x in [:A,A:] holds
(F || A) . x in A

proof

let x be set ; :: 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, Def6; :: thesis: verum

end;

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