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 that
A1: a in dom f and
A2: g = f . a and
A3: b in dom g ; :: thesis: ((commute f) . b) . a = g . b
A4: [a,b] in dom (uncurry f) by A1, A2, A3, FUNCT_5:def 2;
A5: [a,b] `2 = b ;
[a,b] `1 = a ;
then (uncurry f) . (a,b) = g . b by A5, A4, A2, FUNCT_5:def 2;
hence ((commute f) . b) . a = g . b by A4, FUNCT_5:22; :: thesis: verum