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)

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

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

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