let a, b be set ; 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; ( 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 ;
TARSKI:def 3 ( not u in dom (uncurry f) or u in [:(dom f),(proj1 (union (rng f))):] )
assume
u in dom (uncurry f)
;
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;
verum
end;
then A5:
uncurry' (commute f) = uncurry f
by FUNCT_5:50;
hereby ( 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)
;
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;
( 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;
verum
end;
given g being Function such that A11:
a in dom f
and
A12:
g = f . a
and
A13:
b in dom g
; 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; verum