let A, B, C be set ; :: thesis: 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; :: thesis: ( 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 A1: ( A <> {} & B <> {} & f in Funcs A,(Funcs B,C) ) ; :: thesis: 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 g, h be Function; :: thesis: 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 ; :: thesis: ( 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 A2: ( x in A & y in B & f . x = g & (commute f) . y = h ) ; :: thesis: ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C )
A3: ex g being Function st
( g = f & dom g = A & rng g c= Funcs B,C ) by A1, FUNCT_2:def 2;
A4: commute f in Funcs B,(Funcs A,C) by A1, Th85;
set cf = commute f;
A5: ex g being Function st
( g = commute f & dom g = B & rng g c= Funcs A,C ) by A4, FUNCT_2:def 2;
f . x in rng f by A2, A3, FUNCT_1:def 5;
then A6: ex t being Function st
( t = g & dom t = B & rng t c= C ) by A2, A3, FUNCT_2:def 2;
(commute f) . y in rng (commute f) by A2, A5, FUNCT_1:def 5;
then A7: ex t being Function st
( t = h & dom t = A & rng t c= C ) by A2, A5, FUNCT_2:def 2;
set uf = uncurry f;
( [x,y] in dom (uncurry f) & (uncurry f) . x,y = g . y ) by A2, A3, A6, FUNCT_5:45;
hence ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) by A2, A6, A7, FUNCT_5:29; :: thesis: verum