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 object ; :: 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 object , g being Function, b being object such that
A1: u = [a,b] and
A2: a in dom f and
A3: g = f . a and
A4: b in dom g by FUNCT_5:def 2;
g in rng f by A2, A3, FUNCT_1:def 3;
then g c= union (rng f) by ZFMISC_1:74;
then proj1 g c= proj1 (union (rng f)) by XTUPLE_0:8;
hence u in [:(dom f),(proj1 (union (rng f))):] by A1, A2, A4, ZFMISC_1:def 2; :: thesis: verum

end;

then A5: uncurry' (commute f) = uncurry f by FUNCT_5:50;

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 A6: 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 2, RELAT_1:38;
then [a,b] in dom (uncurry f) by A5, A6, FUNCT_5:39;
then consider a9 being object , g being Function, b9 being object such that
A7: [a,b] = [a9,b9] and
A8: a9 in dom f and
A9: g = f . a9 and
A10: b9 in dom g by FUNCT_5:def 2;
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 A7, A8, A9, A10, XTUPLE_0:1; :: thesis: verum

end;

given g being Function such that A11: a in dom f and
A12: g = f . a and
A13: b in dom g ; :: thesis: a in dom ((commute f) . b)
[a,b] in dom (uncurry f) by A11, A12, A13, FUNCT_5:def 2;
hence a in dom ((commute f) . b) by FUNCT_5:22; :: thesis: verum