let X be non empty 1-sorted ; :: thesis: for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
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 I
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 I; :: 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: the carrier of (I -TOP_prod J) = product (Carrier J) by WAYBEL18:def 3;
let i be Element of I; :: thesis: (commute f) . i = (proj J,i) * f
A2: dom (Carrier J) = I by PARTFUN1:def 4;
A3: 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 and
A5: dom h = I and
A6: for x being set st x in I holds
h . x in (Carrier J) . x by A1, A2, 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) )
A7: dom (Carrier J) = I by PARTFUN1:def 4;
assume y in rng h ; :: thesis: y in Union (Carrier J)
then consider x being set such that
A8: x in dom h and
A9: y = h . x by FUNCT_1:def 5;
h . x in (Carrier J) . x by A5, A6, A8;
hence y in Union (Carrier J) by A5, A8, A9, A7, CARD_5:10; :: thesis: verum

end;

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

end;

dom f = the carrier of X by FUNCT_2:def 1;
then A10: f in Funcs the carrier of X,(Funcs I,(Union (Carrier J))) by A3, FUNCT_2:def 2;
then commute f in Funcs I,(Funcs the carrier of X,(Union (Carrier J))) by FUNCT_6:85;
then A11: 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;
then (commute f) . i in rng (commute f) by FUNCT_1:def 5;
then consider g being Function such that
A12: (commute f) . i = g and
A13: dom g = the carrier of X and
rng g c= Union (Carrier J) by A11, FUNCT_2:def 2;

A14: now

let x be set ; :: thesis: ( x in the carrier of X implies g . x = ((proj J,i) * f) . x )
A15: dom (proj (Carrier J),i) = product (Carrier J) by CARD_3:def 17;
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
A16: f . a = h and
dom h = I and
for x being set st x in I holds
h . x in (Carrier J) . x by A1, A2, CARD_3:def 5;
((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 A1, A16, A15, CARD_3:def 17 ;
hence g . x = ((proj J,i) * f) . x by A10, A12, A16, FUNCT_6:86; :: thesis: verum

end;

dom ((proj J,i) * f) = the carrier of X by FUNCT_2:def 1;
hence (commute f) . i = (proj J,i) * f by A12, A13, A14, FUNCT_1:9; :: thesis: verum