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:18
.= F . (x,x) by FUNCT_1:18 ; :: thesis: verum