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