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

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

suppose Y = {} ; :: thesis: F .: f,g = F .: g,f

hence F .: f,g = F .: g,f ; :: thesis: verum

end;

suppose S: Y <> {} ; :: thesis: F .: f,g = F .: g,f

now

let y be Element of Y; :: thesis: (F .: f,g) . y = F . (g . y),(f . y)
reconsider x1 = f . y, x2 = g . y as Element of X by S, FUNCT_2:7;
thus (F .: f,g) . y = F . x1,x2 by S, Th48
.= F . (g . y),(f . y) by A1, BINOP_1:def 2 ; :: thesis: verum

end;

hence F .: f,g = F .: g,f by S, Th49; :: thesis: verum

end;

end;