let D be non empty set ; for RD being Equivalence_Relation of D
for a, b being Element of D
for F being BinOp of D,RD holds (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
let RD be Equivalence_Relation of D; for a, b being Element of D
for F being BinOp of D,RD holds (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
let a, b be Element of D; for F being BinOp of D,RD holds (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
let F be BinOp of D,RD; (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
A1:
b in EqClass (RD,b)
by EQREL_1:20;
a in EqClass (RD,a)
by EQREL_1:20;
hence
(F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))
by A1, Def4; verum