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);
take pr1 (X,X) ; :: thesis: for x being set st x in [:A,A:] holds
(pr1 (X,X)) . x in A
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 object such that
A1: ( p in A & q in A ) and
A2: 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 A1, FUNCT_3:def 4; :: thesis: verum

end;

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