let X, Y be non empty set ; for F being BinOp of X
for f, g being Function of Y,X
for x being Element of X st ( for y being Element of Y holds g . y = F . ((f . y),x) ) holds
g = F [:] (f,x)
let F be BinOp of X; for f, g being Function of Y,X
for x being Element of X st ( for y being Element of Y holds g . y = F . ((f . y),x) ) holds
g = F [:] (f,x)
let f, g be Function of Y,X; for x being Element of X st ( for y being Element of Y holds g . y = F . ((f . y),x) ) holds
g = F [:] (f,x)
let x be Element of X; ( ( for y being Element of Y holds g . y = F . ((f . y),x) ) implies g = F [:] (f,x) )
assume A1:
for y being Element of Y holds g . y = F . ((f . y),x)
; g = F [:] (f,x)
hence
g = F [:] (f,x)
by FUNCT_2:63; verum