let X be non empty 1-sorted ; :: thesis: for I being non empty set
for J being non-Empty TopStruct-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 TopStruct-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 TopStruct-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 2;
A3: rng f c= Funcs (I,(Union (Carrier J)))

proof

let g be object ; :: 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 object 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 object ; :: 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 2;
assume y in rng h ; :: thesis: y in Union (Carrier J)
then consider x being object such that
A8: x in dom h and
A9: y = h . x by FUNCT_1:def 3;
h . x in (Carrier J) . x by A5, A6, A8;
hence y in Union (Carrier J) by A5, A8, A9, A7, CARD_5:2; :: 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:55;
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 3;
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 :: thesis: for x being object st x in the carrier of X holds
g . x = ((proj (J,i)) * f) . x

let x be object ; :: 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 16;
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 object 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:15
.= (proj ((Carrier J),i)) . (f . a) by WAYBEL18:def 4
.= h . i by A1, A16, A15, CARD_3:def 16 ;
hence g . x = ((proj (J,i)) * f) . x by A10, A12, A16, FUNCT_6:56; :: 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:2; :: thesis: verum