let f be Function-yielding Function; :: thesis: for i, A being set st i in dom (commute f) holds
((commute f) . i) .: A c= pi ((f .: A),i)
let i, A be set ; :: thesis: ( i in dom (commute f) implies ((commute f) . i) .: A c= pi ((f .: A),i) )
A1: commute f = curry' (uncurry f) by FUNCT_6:def 10
.= curry (~ (uncurry f)) by FUNCT_5:def 3 ;
assume A2: i in dom (commute f) ; :: thesis: ((commute f) . i) .: A c= pi ((f .: A),i)
thus ((commute f) . i) .: A c= pi ((f .: A),i) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((commute f) . i) .: A or x in pi ((f .: A),i) )
assume x in ((commute f) . i) .: A ; :: thesis: x in pi ((f .: A),i)
then consider y being object such that
A3: y in dom ((commute f) . i) and
A4: y in A and
A5: x = ((commute f) . i) . y by FUNCT_1:def 6;
A6: [i,y] in dom (~ (uncurry f)) by A2, A1, A3, FUNCT_5:31;
then A7: [y,i] in dom (uncurry f) by FUNCT_4:42;
then ex a being object ex g being Function ex b being object st
( [y,i] = [a,b] & a in dom f & g = f . a & b in dom g ) by FUNCT_5:def 2;
then y in dom f by XTUPLE_0:1;
then A8: f . y in f .: A by A4, FUNCT_1:def 6;
A9: [y,i] `2 = i ;
A10: [y,i] `1 = y ;
x = (~ (uncurry f)) . (i,y) by A2, A1, A3, A5, FUNCT_5:31
.= (uncurry f) . (y,i) by A6, FUNCT_4:43
.= (f . y) . i by A7, A10, A9, FUNCT_5:def 2 ;
hence x in pi ((f .: A),i) by A8, CARD_3:def 6; :: thesis: verum

end;