let X be set ; :: thesis: for A being Subset of X ex F being BinOp of X st
for x being set st x in [:A,A:] holds
F . x in A
let A be Subset of X; :: thesis: ex F being BinOp of X st
for x being set st x in [:A,A:] holds
F . x in A
set S = pr1 X,X;
A1: for x being set st x in [:A,A:] holds
(pr1 X,X) . x in A

proof

let x be set ; :: thesis: ( x in [:A,A:] implies (pr1 X,X) . x in A )
assume x in [:A,A:] ; :: thesis: (pr1 X,X) . x in A
then consider p, q being set such that
A2: ( p in A & q in A & x = [p,q] ) by ZFMISC_1:def 2;
(pr1 X,X) . x = (pr1 X,X) . p,q by A2;
hence (pr1 X,X) . x in A by A2, FUNCT_3:def 5; :: thesis: verum

end;

take pr1 X,X ; :: thesis: for x being set st x in [:A,A:] holds
(pr1 X,X) . x in A
thus for x being set st x in [:A,A:] holds
(pr1 X,X) . x in A by A1; :: thesis: verum