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 that
A1: ( A <> {} & B <> {} ) and
A2: f in Funcs (A,(Funcs (B,C))) ; :: thesis: commute (commute f) = f
A3: ex g being Function st
( g = f & dom g = A & rng g c= Funcs (B,C) ) by A2, FUNCT_2:def 2;
set cf = commute f;
A4: commute f in Funcs (B,(Funcs (A,C))) by A1, A2, Th50;
then commute (commute f) in Funcs (A,(Funcs (B,C))) by A1, Th50;
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;
A6: ex g being Function st
( g = commute f & dom g = B & rng g c= Funcs (A,C) ) by A4, FUNCT_2:def 2;
for x being object st x in A holds
f . x = (commute (commute f)) . x

proof

set ccf = commute (commute f);
set uf = uncurry f;
set ucf = uncurry (commute f);
let x be object ; :: thesis: ( x in A implies f . x = (commute (commute f)) . x )
assume A7: x in A ; :: thesis: f . x = (commute (commute f)) . x
then f . x in rng f by A3, FUNCT_1:def 3;
then consider g being Function such that
A8: ( g = f . x & dom g = B ) and
rng g c= C by A3, FUNCT_2:def 2;
(commute (commute f)) . x in rng (commute (commute f)) by A5, A7, FUNCT_1:def 3;
then consider h being Function such that
A9: h = (commute (commute f)) . x and
A10: dom h = B and
rng h c= C by A5, FUNCT_2:def 2;
A11: for y being object 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 object ; :: thesis: ( y in B implies for h being Function st h = (commute f) . y holds
( x in dom h & h . x = g . y ) )
assume y in B ; :: thesis: for h being Function st h = (commute f) . y holds
( x in dom h & h . x = g . y )
then A12: ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y ) by A3, A7, A8, FUNCT_5:38;
let h be Function; :: thesis: ( h = (commute f) . y implies ( x in dom h & h . x = g . y ) )
assume h = (commute f) . y ; :: thesis: ( x in dom h & h . x = g . y )
hence ( x in dom h & h . x = g . y ) by A12, FUNCT_5:22; :: thesis: verum

end;

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

proof

let y be object ; :: thesis: ( y in B implies ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) )
reconsider h = (commute f) . y as Function ;
assume A14: y in B ; :: thesis: ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y )
then ( x in dom h & h . x = g . y ) by A11;
hence ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) by A6, A14, FUNCT_5:38; :: thesis: verum

end;

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

proof

let y be object ; :: 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 A13;
hence h . y = g . y by A9, FUNCT_5:22; :: thesis: verum

end;

hence f . x = (commute (commute f)) . x by A8, A9, A10, FUNCT_1:2; :: thesis: verum

end;

hence commute (commute f) = f by A3, A5; :: thesis: verum