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 . (x,(f . y)) ) holds

g = F [;] (x,f)

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 . (x,(f . y)) ) holds

g = F [;] (x,f)

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 . (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)

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 . (x,(f . y)) ) holds

g = F [;] (x,f)

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 . (x,(f . y)) ) holds

g = F [;] (x,f)

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 . (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 :: thesis: for y being Element of Y holds g . y = (F [;] (x,f)) . y

hence
g = F [;] (x,f)
by FUNCT_2:63; :: thesis: verumlet 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 Th53 ; :: thesis: verum

end;thus g . y = F . (x,(f . y)) by A1

.= (F [;] (x,f)) . y by Th53 ; :: thesis: verum