let A, B, C be set ; for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds
for g, h being Function
for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds
( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C )
let f be Function; ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) implies for g, h being Function
for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds
( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) )
assume that
A1:
( A <> {} & B <> {} )
and
A2:
f in Funcs (A,(Funcs (B,C)))
; for g, h being Function
for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds
( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C )
set uf = uncurry f;
set cf = commute f;
let g, h be Function; for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds
( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C )
let x, y be set ; ( x in A & y in B & f . x = g & (commute f) . y = h implies ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) )
assume that
A3:
x in A
and
A4:
y in B
and
A5:
f . x = g
and
A6:
(commute f) . y = h
; ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C )
commute f in Funcs (B,(Funcs (A,C)))
by A1, A2, Th50;
then A7:
ex g being Function st
( g = commute f & dom g = B & rng g c= Funcs (A,C) )
by FUNCT_2:def 2;
then
(commute f) . y in rng (commute f)
by A4, FUNCT_1:def 3;
then A8:
ex t being Function st
( t = h & dom t = A & rng t c= C )
by A6, A7, FUNCT_2:def 2;
A9:
ex g being Function st
( g = f & dom g = A & rng g c= Funcs (B,C) )
by A2, FUNCT_2:def 2;
then
f . x in rng f
by A3, FUNCT_1:def 3;
then A10:
ex t being Function st
( t = g & dom t = B & rng t c= C )
by A5, A9, FUNCT_2:def 2;
then
( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y )
by A3, A4, A5, A9, FUNCT_5:38;
hence
( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C )
by A6, A10, A8, FUNCT_5:22; verum