let A be non trivial set ; :: thesis: for x being Element of A
for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x})
let x be Element of A; :: thesis: for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x})
let F be DnT of x,A; :: thesis: F || (A \ {x}) is BinOp of (A \ {x})
( dom F = [:A,A:] & rng F c= A ) by FUNCT_2:def 1, RELAT_1:def 19;
then A1: dom (F || (A \ {x})) = [:(A \ {x}),(A \ {x}):] by RELAT_1:91, ZFMISC_1:119;
for y being set st y in [:(A \ {x}),(A \ {x}):] holds
(F || (A \ {x})) . y in A \ {x}

proof

let y be set ; :: thesis: ( y in [:(A \ {x}),(A \ {x}):] implies (F || (A \ {x})) . y in A \ {x} )
assume A2: y in [:(A \ {x}),(A \ {x}):] ; :: thesis: (F || (A \ {x})) . y in A \ {x}
then (F || (A \ {x})) . y = F . y by A1, FUNCT_1:70;
hence (F || (A \ {x})) . y in A \ {x} by A2, Def8; :: thesis: verum

end;

hence F || (A \ {x}) is BinOp of (A \ {x}) by A1, FUNCT_2:5; :: thesis: verum