let X, Y be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 f or f . x is set )
assume x in dom f ; :: thesis: f . x is set
then f . x in rng f by FUNCT_1:def 5;
hence f . x is set by A1; :: thesis: verum

end;

let i, A be set ; :: thesis: ( i in X implies ((commute f) . i) .: A = pi (f .: A),i )
assume A4: i in X ; :: thesis: ((commute f) . i) .: A = pi (f .: A),i

per cases ( dom f = {} or dom f <> {} ) ;

suppose dom f = {} ; :: thesis: ((commute f) . i) .: A = pi (f .: A),i

then A5: f = {} ;
then (commute f) . i = {} by FUNCT_1:def 4, FUNCT_6:88, RELAT_1:60;
then A6: ((commute f) . i) .: A = {} by RELAT_1:150;
f .: A = {} by A5, RELAT_1:150;
hence ((commute f) . i) .: A = pi (f .: A),i by A6, CARD_3:24; :: thesis: verum

end;

suppose dom f <> {} ; :: thesis: ((commute f) . i) .: A = pi (f .: A),i

then commute f in Funcs X,(Funcs (dom f),Y) by A2, A4, FUNCT_6:85;
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; :: according to XBOOLE_0:def 10 :: thesis: pi (f .: A),i c= ((commute f) . i) .: A

now

let g be Function; :: thesis: ( g in f .: A implies i in dom g )
A7: f .: A c= rng f by RELAT_1:144;
assume g in f .: A ; :: thesis: i in dom g
then g in rng f by A7;
then ex h being Function st
( g = h & dom h = X & rng h c= Y ) by A1, FUNCT_2:def 2;
hence i in dom g by A4; :: thesis: verum

end;

hence pi (f .: A),i c= ((commute f) . i) .: A by A3, Th7; :: thesis: verum

end;

end;