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

now

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

end;

hence g = F [;] x,f by FUNCT_2:113; :: thesis: verum