let X, Y be non empty set ; :: thesis: for F being BinOp of X
for f, g being Function of Y,X
for z being Element of Y holds (F .: f,g) . z = F . (f . z),(g . z)
let F be BinOp of X; :: thesis: for f, g being Function of Y,X
for z being Element of Y holds (F .: f,g) . z = F . (f . z),(g . z)
let f, g be Function of Y,X; :: thesis: for z being Element of Y holds (F .: f,g) . z = F . (f . z),(g . z)
let z be Element of Y; :: thesis: (F .: f,g) . z = F . (f . z),(g . z)
dom (F .: f,g) = Y by FUNCT_2:def 1;
hence (F .: f,g) . z = F . (f . z),(g . z) by Lm1; :: thesis: verum