let X, Y be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: g = F [:] (f,x)

now :: thesis: for y being Element of Y holds g . y = (F [:] (f,x)) . y

let y be Element of Y; :: thesis: g . y = (F [:] (f,x)) . y
thus g . y = F . ((f . y),x) by A1
.= (F [:] (f,x)) . y by Th48 ; :: thesis: verum

end;

hence g = F [:] (f,x) by FUNCT_2:63; :: thesis: verum