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

end;