let f be Function; 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 ; ( [:A,{i}:] c= dom f implies pi (((curry f) .: A),i) = f .: [:A,{i}:] )
assume A1:
[:A,{i}:] c= dom f
; 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}:]
XBOOLE_0:def 10 f .: [:A,{i}:] c= pi (((curry f) .: A),i)proof
let x be
object ;
TARSKI:def 3 ( not x in pi (((curry f) .: A),i) or x in f .: [:A,{i}:] )
assume
x in pi (
((curry f) .: A),
i)
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in f .: [:A,{i}:] or x in pi (((curry f) .: A),i) )
assume
x in f .: [:A,{i}:]
; 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; verum