let a, b be set ; :: thesis: for f being Function holds
( a in dom ((commute f) . b) iff ex g being Function st
( a in dom f & g = f . a & b in dom g ) )
let f be Function; :: thesis: ( a in dom ((commute f) . b) iff ex g being Function st
( a in dom f & g = f . a & b in dom g ) )
dom (uncurry f) c= [:(dom f),(proj1 (union (rng f))):]

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in dom (uncurry f) or u in [:(dom f),(proj1 (union (rng f))):] )
assume u in dom (uncurry f) ; :: thesis: u in [:(dom f),(proj1 (union (rng f))):]
then consider a being set , g being Function, b being set such that
A1: ( u = [a,b] & a in dom f & g = f . a & b in dom g ) by FUNCT_5:def 4;
g in rng f by A1, FUNCT_1:def 5;
then g c= union (rng f) by ZFMISC_1:92;
then ( proj1 g = dom g & proj1 g c= proj1 (union (rng f)) ) by FUNCT_5:5;
hence u in [:(dom f),(proj1 (union (rng f))):] by A1, ZFMISC_1:def 2; :: thesis: verum

end;

then A2: uncurry' (commute f) = uncurry f by FUNCT_5:57;

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

assume A3: a in dom ((commute f) . b) ; :: thesis: ex g being Function st
( a in dom f & g = f . a & b in dom g )
then b in dom (commute f) by FUNCT_1:def 4, RELAT_1:60;
then [a,b] in dom (uncurry f) by A2, A3, FUNCT_5:46;
then consider a' being set , g being Function, b' being set such that
A4: ( [a,b] = [a',b'] & a' in dom f & g = f . a' & b' in dom g ) by FUNCT_5:def 4;
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 A4, ZFMISC_1:33; :: thesis: verum

end;

given g being Function such that A5: ( a in dom f & g = f . a & b in dom g ) ; :: thesis: a in dom ((commute f) . b)
( [a,b] `1 = a & [a,b] `2 = b & [a,b] in dom (uncurry f) ) by A5, FUNCT_5:def 4, MCART_1:7;
hence a in dom ((commute f) . b) by FUNCT_5:29; :: thesis: verum