let X be non empty set ; :: thesis: for F being BinOp of X
for x being Element of X holds (F [;] x,(id X)) . x = F . x,x
let F be BinOp of X; :: thesis: for x being Element of X holds (F [;] x,(id X)) . x = F . x,x
let x be Element of X; :: thesis: (F [;] x,(id X)) . x = F . x,x
thus (F [;] x,(id X)) . x = F . x,((id X) . x) by Th66
.= F . x,x by FUNCT_1:35 ; :: thesis: verum