let A, B, C be set ; :: thesis: for f being Function st A <> {} & B <> {} & f in Funcs A,(Funcs B,C) holds
commute (commute f) = f
let f be Function; :: thesis: ( A <> {} & B <> {} & f in Funcs A,(Funcs B,C) implies commute (commute f) = f )
assume A1: ( A <> {} & B <> {} & f in Funcs A,(Funcs B,C) ) ; :: thesis: commute (commute f) = f
then A2: ex g being Function st
( g = f & dom g = A & rng g c= Funcs B,C ) by FUNCT_2:def 2;
A3: commute f in Funcs B,(Funcs A,C) by A1, Th85;
set cf = commute f;
A4: ex g being Function st
( g = commute f & dom g = B & rng g c= Funcs A,C ) by A3, FUNCT_2:def 2;
commute (commute f) in Funcs A,(Funcs B,C) by A1, A3, Th85;
then A5: ex h being Function st
( h = commute (commute f) & dom h = A & rng h c= Funcs B,C ) by FUNCT_2:def 2;
for x being set st x in A holds
f . x = (commute (commute f)) . x

proof

let x be set ; :: thesis: ( x in A implies f . x = (commute (commute f)) . x )
assume A6: x in A ; :: thesis: f . x = (commute (commute f)) . x
then f . x in rng f by A2, FUNCT_1:def 5;
then consider g being Function such that
A7: ( g = f . x & dom g = B & rng g c= C ) by A2, FUNCT_2:def 2;
set ccf = commute (commute f);
set uf = uncurry f;
set ucf = uncurry (commute f);
(commute (commute f)) . x in rng (commute (commute f)) by A5, A6, FUNCT_1:def 5;
then consider h being Function such that
A8: ( h = (commute (commute f)) . x & dom h = B & rng h c= C ) by A5, FUNCT_2:def 2;
A9: for y being set st y in B holds
for h being Function st h = (commute f) . y holds
( x in dom h & h . x = g . y )

proof

let y be set ; :: thesis: ( y in B implies for h being Function st h = (commute f) . y holds
( x in dom h & h . x = g . y ) )
assume A10: y in B ; :: thesis: for h being Function st h = (commute f) . y holds
( x in dom h & h . x = g . y )
let h be Function; :: thesis: ( h = (commute f) . y implies ( x in dom h & h . x = g . y ) )
assume A11: h = (commute f) . y ; :: thesis: ( x in dom h & h . x = g . y )
( [x,y] in dom (uncurry f) & (uncurry f) . x,y = g . y ) by A2, A6, A7, A10, FUNCT_5:45;
hence ( x in dom h & h . x = g . y ) by A11, FUNCT_5:29; :: thesis: verum

end;

A12: for y being set st y in B holds
( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . y,x = g . y )

proof

let y be set ; :: thesis: ( y in B implies ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . y,x = g . y ) )
assume A13: y in B ; :: thesis: ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . y,x = g . y )
reconsider h = (commute f) . y as Function ;
( x in dom h & h . x = g . y ) by A9, A13;
hence ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . y,x = g . y ) by A4, A13, FUNCT_5:45; :: thesis: verum

end;

for y being set st y in B holds
h . y = g . y

proof

let y be set ; :: thesis: ( y in B implies h . y = g . y )
assume y in B ; :: thesis: h . y = g . y
then ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . y,x = g . y ) by A12;
hence h . y = g . y by A8, FUNCT_5:29; :: thesis: verum

end;

hence f . x = (commute (commute f)) . x by A7, A8, FUNCT_1:9; :: thesis: verum

end;

hence commute (commute f) = f by A2, A5, FUNCT_1:9; :: thesis: verum