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