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 Th37

.= F . (x,(g . x)) ; :: thesis: verum

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 Th37

.= F . (x,(g . x)) ; :: thesis: verum