let A, B, C be set ; :: thesis: for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds
commute f in Funcs (B,(Funcs (A,C)))
let f be Function; :: thesis: ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) implies commute f in Funcs (B,(Funcs (A,C))) )
assume ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) ) ; :: thesis: commute f in Funcs (B,(Funcs (A,C)))
then ( [:A,B:] <> {} & uncurry f in Funcs ([:A,B:],C) ) by Th11, ZFMISC_1:90;
hence commute f in Funcs (B,(Funcs (A,C))) by Th10; :: thesis: verum