let f be Function; :: thesis: for i, A being set st [:A,{i}:] c= dom f holds
pi ((curry f) .: A),i = f .: [:A,{i}:]
let i, A be set ; :: thesis: ( [:A,{i}:] c= dom f implies pi ((curry f) .: A),i = f .: [:A,{i}:] )
assume A1: [:A,{i}:] c= dom f ; :: thesis: pi ((curry f) .: A),i = f .: [:A,{i}:]
A2: i in {i} by TARSKI:def 1;
thus pi ((curry f) .: A),i c= f .: [:A,{i}:] :: according to XBOOLE_0:def 10 :: thesis: f .: [:A,{i}:] c= pi ((curry f) .: A),i

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in pi ((curry f) .: A),i or x in f .: [:A,{i}:] )
assume x in pi ((curry f) .: A),i ; :: thesis: x in f .: [:A,{i}:]
then consider g being Function such that
A3: ( g in (curry f) .: A & x = g . i ) by CARD_3:def 6;
consider a being set such that
A4: ( a in dom (curry f) & a in A & g = (curry f) . a ) by A3, FUNCT_1:def 12;
A5: [a,i] in [:A,{i}:] by A2, A4, ZFMISC_1:def 2;
then f . a,i in f .: [:A,{i}:] by A1, FUNCT_1:def 12;
hence x in f .: [:A,{i}:] by A1, A3, A4, A5, FUNCT_5:27; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: [:A,{i}:] or x in pi ((curry f) .: A),i )
assume x in f .: [:A,{i}:] ; :: thesis: x in pi ((curry f) .: A),i
then consider y being set such that
A6: ( y in dom f & y in [:A,{i}:] & x = f . y ) by FUNCT_1:def 12;
consider y1, y2 being set such that
A7: ( y1 in A & y2 in {i} & y = [y1,y2] ) by A6, ZFMISC_1:def 2;
reconsider g = (curry f) . y1 as Function by A6, A7, FUNCT_5:26;
A8: x = f . y1,y2 by A6, A7;
y2 = i by A7, TARSKI:def 1;
then A9: x = g . i by A6, A7, A8, FUNCT_5:27;
y1 in dom (curry f) by A6, A7, FUNCT_5:26;
then g in (curry f) .: A by A7, FUNCT_1:def 12;
hence x in pi ((curry f) .: A),i by A9, CARD_3:def 6; :: thesis: verum