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 Th32; :: thesis: verum

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 Th32; :: thesis: verum