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

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