let X, Y be set ; for f being Function st rng f c= Funcs (X,Y) holds
for i, A being set st i in X holds
((commute f) . i) .: A = pi ((f .: A),i)
let f be Function; ( rng f c= Funcs (X,Y) implies for i, A being set st i in X holds
((commute f) . i) .: A = pi ((f .: A),i) )
assume A1:
rng f c= Funcs (X,Y)
; for i, A being set st i in X holds
((commute f) . i) .: A = pi ((f .: A),i)
then A2:
f in Funcs ((dom f),(Funcs (X,Y)))
by FUNCT_2:def 2;
A3:
f is Function-yielding
let i, A be set ; ( i in X implies ((commute f) . i) .: A = pi ((f .: A),i) )
assume A4:
i in X
; ((commute f) . i) .: A = pi ((f .: A),i)
per cases
( dom f = {} or dom f <> {} )
;
suppose
dom f <> {}
;
((commute f) . i) .: A = pi ((f .: A),i)then
commute f in Funcs (
X,
(Funcs ((dom f),Y)))
by A2, A4, FUNCT_6:55;
then
ex
g being
Function st
(
commute f = g &
dom g = X &
rng g c= Funcs (
(dom f),
Y) )
by FUNCT_2:def 2;
hence
((commute f) . i) .: A c= pi (
(f .: A),
i)
by A3, A4, Th6;
XBOOLE_0:def 10 pi ((f .: A),i) c= ((commute f) . i) .: Ahence
pi (
(f .: A),
i)
c= ((commute f) . i) .: A
by A3, Th7;
verum end; end;