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 and
A4: x = g . i by CARD_3:def 6;
consider a being set such that
a in dom (curry f) and
A5: a in A and
A6: g = (curry f) . a by A3, FUNCT_1:def 12;
A7: [a,i] in [:A,{i}:] by A2, A5, 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, A4, A6, A7, 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
A8: y in dom f and
A9: y in [:A,{i}:] and
A10: x = f . y by FUNCT_1:def 12;
consider y1, y2 being set such that
A11: y1 in A and
A12: y2 in {i} and
A13: y = [y1,y2] by A9, ZFMISC_1:def 2;
reconsider g = (curry f) . y1 as Function by A8, A13, FUNCT_5:26;
y1 in dom (curry f) by A8, A13, FUNCT_5:26;
then A14: g in (curry f) .: A by A11, FUNCT_1:def 12;
A15: y2 = i by A12, TARSKI:def 1;
x = f . y1,y2 by A10, A13;
then x = g . i by A15, A8, A13, FUNCT_5:27;
hence x in pi ((curry f) .: A),i by A14, CARD_3:def 6; :: thesis: verum