let X be non empty 1-sorted ; :: thesis: for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of
for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj J,i) * f
let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj J,i) * f
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis: for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj J,i) * f
let f be Function of X,(I -TOP_prod J); :: thesis: for i being Element of I holds (commute f) . i = (proj J,i) * f
A1: ( dom f = the carrier of X & rng f c= the carrier of (I -TOP_prod J) ) by FUNCT_2:def 1;
A2: the carrier of (I -TOP_prod J) = product (Carrier J) by WAYBEL18:def 3;
A3: dom (Carrier J) = I by PARTFUN1:def 4;
rng f c= Funcs I,(Union (Carrier J))

proof

let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in rng f or g in Funcs I,(Union (Carrier J)) )
assume g in rng f ; :: thesis: g in Funcs I,(Union (Carrier J))
then consider h being Function such that
A4: ( g = h & dom h = I & ( for x being set st x in I holds
h . x in (Carrier J) . x ) ) by A2, A3, CARD_3:def 5;
rng h c= Union (Carrier J)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h or y in Union (Carrier J) )
assume y in rng h ; :: thesis: y in Union (Carrier J)
then consider x being set such that
A5: ( x in dom h & y = h . x ) by FUNCT_1:def 5;
( h . x in (Carrier J) . x & dom (Carrier J) = I ) by A4, A5, PARTFUN1:def 4;
hence y in Union (Carrier J) by A4, A5, CARD_5:10; :: thesis: verum

end;

hence g in Funcs I,(Union (Carrier J)) by A4, FUNCT_2:def 2; :: thesis: verum

end;

then A6: f in Funcs the carrier of X,(Funcs I,(Union (Carrier J))) by A1, FUNCT_2:def 2;
then commute f in Funcs I,(Funcs the carrier of X,(Union (Carrier J))) by FUNCT_6:85;
then A7: ex g being Function st
( commute f = g & dom g = I & rng g c= Funcs the carrier of X,(Union (Carrier J)) ) by FUNCT_2:def 2;
let i be Element of I; :: thesis: (commute f) . i = (proj J,i) * f
(commute f) . i in rng (commute f) by A7, FUNCT_1:def 5;
then consider g being Function such that
A8: (commute f) . i = g and
A9: dom g = the carrier of X and
rng g c= Union (Carrier J) by A7, FUNCT_2:def 2;
A10: dom ((proj J,i) * f) = the carrier of X by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in the carrier of X implies g . x = ((proj J,i) * f) . x )
assume x in the carrier of X ; :: thesis: g . x = ((proj J,i) * f) . x
then reconsider a = x as Element of X ;
consider h being Function such that
A11: ( f . a = h & dom h = I & ( for x being set st x in I holds
h . x in (Carrier J) . x ) ) by A2, A3, CARD_3:def 5;
A12: dom (proj (Carrier J),i) = product (Carrier J) by PRALG_3:def 2;
((proj J,i) * f) . a = (proj J,i) . (f . a) by FUNCT_2:21
.= (proj (Carrier J),i) . (f . a) by WAYBEL18:def 4
.= h . i by A2, A11, A12, PRALG_3:def 2 ;
hence g . x = ((proj J,i) * f) . x by A6, A8, A11, FUNCT_6:86; :: thesis: verum

end;

hence (commute f) . i = (proj J,i) * f by A8, A9, A10, FUNCT_1:9; :: thesis: verum