let f be Function-yielding Function; for i, A being set st ( for g being Function st g in f .: A holds
i in dom g ) holds
pi ((f .: A),i) c= ((commute f) . i) .: A
let i, A be set ; ( ( for g being Function st g in f .: A holds
i in dom g ) implies pi ((f .: A),i) c= ((commute f) . i) .: A )
assume A1:
for g being Function st g in f .: A holds
i in dom g
; pi ((f .: A),i) c= ((commute f) . i) .: A
let x be object ; TARSKI:def 3 ( not x in pi ((f .: A),i) or x in ((commute f) . i) .: A )
assume
x in pi ((f .: A),i)
; x in ((commute f) . i) .: A
then consider g being Function such that
A2:
g in f .: A
and
A3:
x = g . i
by CARD_3:def 6;
consider y being object such that
A4:
y in dom f
and
A5:
y in A
and
A6:
g = f . y
by A2, FUNCT_1:def 6;
i in dom g
by A1, A2;
then A7:
[y,i] in dom (uncurry f)
by A4, A6, FUNCT_5:def 2;
then A8:
[i,y] in dom (~ (uncurry f))
by FUNCT_4:def 2;
then A9:
i in proj1 (dom (~ (uncurry f)))
by XTUPLE_0:def 12;
then A10:
i in dom (curry (~ (uncurry f)))
by FUNCT_5:def 1;
A11:
i in {i}
by TARSKI:def 1;
y in proj2 (dom (~ (uncurry f)))
by A8, XTUPLE_0:def 13;
then
[i,y] in [:{i},(proj2 (dom (~ (uncurry f)))):]
by A11, ZFMISC_1:87;
then A12:
[i,y] in (dom (~ (uncurry f))) /\ [:{i},(proj2 (dom (~ (uncurry f)))):]
by A8, XBOOLE_0:def 4;
then A13:
y in proj2 ((dom (~ (uncurry f))) /\ [:{i},(proj2 (dom (~ (uncurry f)))):])
by XTUPLE_0:def 13;
A14:
[y,i] `2 = i
;
A15:
[y,i] `1 = y
;
A16: commute f =
curry' (uncurry f)
by FUNCT_6:def 10
.=
curry (~ (uncurry f))
by FUNCT_5:def 3
;
A17:
ex h being Function st
( (curry (~ (uncurry f))) . i = h & dom h = proj2 ((dom (~ (uncurry f))) /\ [:{i},(proj2 (dom (~ (uncurry f)))):]) & ( for b being object st b in dom h holds
h . b = (~ (uncurry f)) . (i,b) ) )
by A9, FUNCT_5:def 1;
then
y in dom ((commute f) . i)
by A16, A12, XTUPLE_0:def 13;
then ((commute f) . i) . y =
(~ (uncurry f)) . (i,y)
by A16, A10, FUNCT_5:31
.=
(uncurry f) . (y,i)
by A7, FUNCT_4:def 2
.=
x
by A3, A6, A7, A15, A14, FUNCT_5:def 2
;
hence
x in ((commute f) . i) .: A
by A5, A16, A17, A13, FUNCT_1:def 6; verum