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 12
.= curry (~ (uncurry f)) by FUNCT_5:def 5 ;
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 set ; :: 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 set 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 12;
A6: [i,y] in dom (~ (uncurry f)) by A2, A1, A3, FUNCT_5:38;
then A7: [y,i] in dom (uncurry f) by FUNCT_4:43;
then ex a being set ex g being Function ex b being set st
( [y,i] = [a,b] & a in dom f & g = f . a & b in dom g ) by FUNCT_5:def 4;
then y in dom f by ZFMISC_1:33;
then A8: f . y in f .: A by A4, FUNCT_1:def 12;
A9: [y,i] `2 = i by MCART_1:7;
A10: [y,i] `1 = y by MCART_1:7;
x = (~ (uncurry f)) . (i,y) by A2, A1, A3, A5, FUNCT_5:38
.= (uncurry f) . (y,i) by A6, FUNCT_4:44
.= (f . y) . i by A7, A10, A9, FUNCT_5:def 4 ;
hence x in pi ((f .: A),i) by A8, CARD_3:def 6; :: thesis: verum

end;