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 Th20, ZFMISC_1:113;
hence commute f in Funcs B,(Funcs A,C) by Th19; :: thesis: verum