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