let b be set ; :: thesis: for f being Function holds
( b in dom (commute f) iff ex a being set ex g being Function st
( a in dom f & g = f . a & b in dom g ) )
let f be Function; :: thesis: ( b in dom (commute f) iff ex a being set ex g being Function st
( a in dom f & g = f . a & b in dom g ) )
A1: dom (commute f) = proj2 (dom (uncurry f)) by FUNCT_5:23;

hereby :: thesis: ( ex a being set ex g being Function st
( a in dom f & g = f . a & b in dom g ) implies b in dom (commute f) )

assume b in dom (commute f) ; :: thesis: ex a being set ex g being Function st
( a in dom f & g = f . a & b in dom g )
then consider a being set such that
A2: [a,b] in dom (uncurry f) by A1, RELAT_1:def 5;
consider a9 being set , g being Function, b9 being set such that
A3: [a,b] = [a9,b9] and
A4: a9 in dom f and
A5: g = f . a9 and
A6: b9 in dom g by A2, FUNCT_5:def 2;
take a = a; :: thesis: ex g being Function st
( a in dom f & g = f . a & b in dom g )
take g = g; :: thesis: ( a in dom f & g = f . a & b in dom g )
thus ( a in dom f & g = f . a & b in dom g ) by A3, A4, A5, A6, ZFMISC_1:27; :: thesis: verum

end;

given a being set , g being Function such that A7: a in dom f and
A8: g = f . a and
A9: b in dom g ; :: thesis: b in dom (commute f)
[a,b] in dom (uncurry f) by A7, A8, A9, FUNCT_5:def 2;
hence b in dom (commute f) by A1, RELAT_1:def 5; :: thesis: verum