let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: (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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: (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; :: thesis: verum