let X be non empty set ; for F being BinOp of X
for x being Element of X
for g being Function of X,X holds (F .: (g,(id X))) . x = F . ((g . x),x)
let F be BinOp of X; for x being Element of X
for g being Function of X,X holds (F .: (g,(id X))) . x = F . ((g . x),x)
let x be Element of X; for g being Function of X,X holds (F .: (g,(id X))) . x = F . ((g . x),x)
let g be Function of X,X; (F .: (g,(id X))) . x = F . ((g . x),x)
thus (F .: (g,(id X))) . x =
F . ((g . x),((id X) . x))
by Th37
.=
F . ((g . x),x)
; verum