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 object ; :: 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 object such that
a in dom (curry f) and
A5: a in A and
A6: g = (curry f) . a by A3, FUNCT_1:def 6;
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 6;
hence x in f .: [:A,{i}:] by A1, A4, A6, A7, FUNCT_5:20; :: thesis: verum

end;

let x be object ; :: 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 object such that
A8: y in dom f and
A9: y in [:A,{i}:] and
A10: x = f . y by FUNCT_1:def 6;
consider y1, y2 being object 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 ;
y1 in dom (curry f) by A8, A13, FUNCT_5:19;
then A14: g in (curry f) .: A by A11, FUNCT_1:def 6;
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:20;
hence x in pi (((curry f) .: A),i) by A14, CARD_3:def 6; :: thesis: verum