let a, b be set ; :: thesis: for f, g being Function st a in dom f & g = f . a & b in dom g holds
((commute f) . b) . a = g . b
let f, g be Function; :: thesis: ( a in dom f & g = f . a & b in dom g implies ((commute f) . b) . a = g . b )
assume A1: ( a in dom f & g = f . a & b in dom g ) ; :: thesis: ((commute f) . b) . a = g . b
then A2: ( [a,b] `1 = a & [a,b] `2 = b & [a,b] in dom (uncurry f) ) by FUNCT_5:def 4, MCART_1:7;
then (uncurry f) . a,b = g . b by A1, FUNCT_5:def 4;
hence ((commute f) . b) . a = g . b by A2, FUNCT_5:29; :: thesis: verum