let X be set ; :: thesis: for F being BinOp of X
for A being Preserv of F holds F || A is BinOp of A
let F be BinOp of X; :: thesis: for A being Preserv of F holds F || A is BinOp of A
let A be Preserv of F; :: thesis: F || A is BinOp of A
( X = {} implies [:X,X:] = {} ) ;
then ( dom F = [:X,X:] & rng F c= X ) by FUNCT_2:def 1, RELAT_1:def 19;
then A1: dom (F || A) = [:A,A:] by RELAT_1:91, ZFMISC_1:119;
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:70;
hence (F || A) . x in A by A2, Def2; :: thesis: verum

end;

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