let X, Y be non empty set ; :: thesis: for F being BinOp of X
for f being Function of Y,X
for x being Element of X
for y being Element of Y holds (F [;] x,f) . y = F . x,(f . y)
let F be BinOp of X; :: thesis: for f being Function of Y,X
for x being Element of X
for y being Element of Y holds (F [;] x,f) . y = F . x,(f . y)
let f be Function of Y,X; :: thesis: for x being Element of X
for y being Element of Y holds (F [;] x,f) . y = F . x,(f . y)
let x be Element of X; :: thesis: for y being Element of Y holds (F [;] x,f) . y = F . x,(f . y)
let y be Element of Y; :: thesis: (F [;] x,f) . y = F . x,(f . y)
dom (F [;] x,f) = Y by FUNCT_2:def 1;
hence (F [;] x,f) . y = F . x,(f . y) by Th42; :: thesis: verum