defpred S1[ Element of Class E, Element of Class E, set ] means for x, y being Element of X st $1 = Class (E,x) & $2 = Class (E,y) holds
$3 = Class (E,(x \ y));
A1:
for W1, W2 being Element of Class E ex V being Element of Class E st S1[W1,W2,V]
proof
let W1,
W2 be
Element of
Class E;
ex V being Element of Class E st S1[W1,W2,V]
consider x1 being
object such that A2:
x1 in the
carrier of
X
and A3:
W1 = Class (
E,
x1)
by EQREL_1:def 3;
consider y1 being
object such that A4:
y1 in the
carrier of
X
and A5:
W2 = Class (
E,
y1)
by EQREL_1:def 3;
reconsider x1 =
x1,
y1 =
y1 as
Element of
X by A2, A4;
reconsider C =
Class (
E,
(x1 \ y1)) as
Element of
Class E by EQREL_1:def 3;
take
C
;
S1[W1,W2,C]
now for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
C = Class (E,(x \ y))let x,
y be
Element of
X;
( W1 = Class (E,x) & W2 = Class (E,y) implies C = Class (E,(x \ y)) )assume that A6:
W1 = Class (
E,
x)
and A7:
W2 = Class (
E,
y)
;
C = Class (E,(x \ y))
y in Class (
E,
y1)
by A5, A7, EQREL_1:23;
then A8:
[y1,y] in E
by EQREL_1:18;
x in Class (
E,
x1)
by A3, A6, EQREL_1:23;
then
[x1,x] in E
by EQREL_1:18;
then
[(x1 \ y1),(x \ y)] in E
by A8, Def9;
then
x \ y in Class (
E,
(x1 \ y1))
by EQREL_1:18;
hence
C = Class (
E,
(x \ y))
by EQREL_1:23;
verum end;
hence
S1[
W1,
W2,
C]
;
verum
end;
thus
ex B being BinOp of (Class E) st
for W1, W2 being Element of Class E holds S1[W1,W2,B . (W1,W2)]
from BINOP_1:sch 3(A1); verum