let D be non empty set ; :: thesis: for d being Element of D
for g being BinOp of D holds g "**" (1 |-> d) = d
let d be Element of D; :: thesis: for g being BinOp of D holds g "**" (1 |-> d) = d
let g be BinOp of D; :: thesis: g "**" (1 |-> d) = d
thus g "**" (1 |-> d) = g "**" <*d*> by FINSEQ_2:59
.= d by Lm4 ; :: thesis: verum