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 object ; :: 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 3;
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_6:58;
then A6: ((commute f) . i) .: A = {} ;
f .: A = {} by A5;
hence ((commute f) . i) .: A = pi ((f .: A),i) by A6, CARD_3:13; :: 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: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; :: according to XBOOLE_0:def 10 :: thesis: pi ((f .: A),i) c= ((commute f) . i) .: A
now :: thesis: for g being Function st g in f .: A holds
i in dom g
let g be Function; :: thesis: ( g in f .: A implies i in dom g )
A7: f .: A c= rng f by RELAT_1:111;
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;