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)

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

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

hence F [;] (x,f) = F [:] (f,x) ; :: thesis: verum

end;

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

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

let 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;

hence F [;] (x,f) = F [:] (f,x) by A2, Th49; :: thesis: verum

end;

end;