let A be non trivial set ; :: thesis: for x being Element of A
for F being A \ {b1} -subsetpreserving BinOp of A holds F || (A \ {x}) is BinOp of (A \ {x})
let x be Element of A; :: thesis: for F being A \ {x} -subsetpreserving BinOp of A holds F || (A \ {x}) is BinOp of (A \ {x})
let F be A \ {x} -subsetpreserving BinOp of A; :: thesis: F || (A \ {x}) is BinOp of (A \ {x})
dom F = [:A,A:] by FUNCT_2:def 1;
then A1: dom (F || (A \ {x})) = [:(A \ {x}),(A \ {x}):] by RELAT_1:62, ZFMISC_1:96;
for y being object st y in [:(A \ {x}),(A \ {x}):] holds
(F || (A \ {x})) . y in A \ {x}
proof
let y be object ; :: 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:47;
hence (F || (A \ {x})) . y in A \ {x} by A2, Def4; :: thesis: verum
end;
hence F || (A \ {x}) is BinOp of (A \ {x}) by A1, FUNCT_2:3; :: thesis: verum