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:30;

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 a' being set , g being Function, b' being set such that
A3: ( [a,b] = [a',b'] & a' in dom f & g = f . a' & b' in dom g ) by A2, FUNCT_5:def 4;
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, ZFMISC_1:33; :: thesis: verum

end;

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