let X be non empty set ; :: thesis: for Y being set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

let Y be set ; :: thesis: for F being BinOp of X

for f being Function of Y,X

for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

let F be BinOp of X; :: thesis: for f being Function of Y,X

for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

let f be Function of Y,X; :: thesis: for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

let x be Element of X; :: thesis: ( F is commutative implies F [;] (x,f) = F [:] (f,x) )

assume A1: F is commutative ; :: thesis: F [;] (x,f) = F [:] (f,x)

for F being BinOp of X

for f being Function of Y,X

for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

let Y be set ; :: thesis: for F being BinOp of X

for f being Function of Y,X

for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

let F be BinOp of X; :: thesis: for f being Function of Y,X

for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

let f be Function of Y,X; :: thesis: for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

let x be Element of X; :: thesis: ( F is commutative implies F [;] (x,f) = F [:] (f,x) )

assume A1: F is commutative ; :: thesis: F [;] (x,f) = F [:] (f,x)

per cases
( Y = {} or Y <> {} )
;

end;

suppose A2:
Y <> {}
; :: thesis: F [;] (x,f) = F [:] (f,x)

end;

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

hence
F [;] (x,f) = F [:] (f,x)
by A2, Th49; :: thesis: verumlet y be Element of Y; :: thesis: (F [;] (x,f)) . y = F . ((f . y),x)

reconsider x1 = f . y as Element of X by A2, FUNCT_2:5;

thus (F [;] (x,f)) . y = F . (x,x1) by A2, Th53

.= F . ((f . y),x) by A1 ; :: thesis: verum

end;reconsider x1 = f . y as Element of X by A2, FUNCT_2:5;

thus (F [;] (x,f)) . y = F . (x,x1) by A2, Th53

.= F . ((f . y),x) by A1 ; :: thesis: verum