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:28;
a in EqClass RD,a by EQREL_1:28;
hence (F /\/ RD) . (Class RD,a),(Class RD,b) = Class RD,(F . a,b) by A1, Def4; :: thesis: verum