let I be non empty set ; for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for y being Function st y in sum (Union F) holds
ex x being Function st
( y = (dprod2prod F) . x & x in dsum F )
let J be non-empty disjoint_valued ManySortedSet of I; for F being Group-Family of I,J
for y being Function st y in sum (Union F) holds
ex x being Function st
( y = (dprod2prod F) . x & x in dsum F )
let F be Group-Family of I,J; for y being Function st y in sum (Union F) holds
ex x being Function st
( y = (dprod2prod F) . x & x in dsum F )
let y be Function; ( y in sum (Union F) implies ex x being Function st
( y = (dprod2prod F) . x & x in dsum F ) )
A1:
[#] (sum (Union F)) c= [#] (product (Union F))
by GROUP_2:def 5;
assume A2:
y in sum (Union F)
; ex x being Function st
( y = (dprod2prod F) . x & x in dsum F )
then reconsider y = y as Element of (product (Union F)) by A1;
A3:
( y in product (Union F) & support (y,(Union F)) is finite )
by A2;
rng (dprod2prod F) = [#] (product (Union F))
by FUNCT_2:def 3;
then consider x being Element of [#] (dprod F) such that
A4:
y = (dprod2prod F) . x
by FUNCT_2:113;
reconsider x = x as Function ;
take
x
; ( y = (dprod2prod F) . x & x in dsum F )
A5:
x in dprod F
;
set sry = supp_restr (y,F);
A6:
support (y,(Union F)) = Union (supp_restr (y,F))
by Th28;
A7:
for i being Element of I holds x . i in (sum_bundle F) . i
proof
let i be
Element of
I;
x . i in (sum_bundle F) . i
i in I
;
then
i in dom (supp_restr (y,F))
by PARTFUN1:def 2;
then A8:
(supp_restr (y,F)) . i c= Union (supp_restr (y,F))
by FUNCT_1:3, ZFMISC_1:74;
A9:
support (
(y | (J . i)),
(F . i)) is
finite
by A2, A6, A8, Def12;
A10:
y | (J . i) = x . i
by A4, Def10;
x . i in (prod_bundle F) . i
by A5, GROUP_19:5;
then
x . i in product (F . i)
by Def6;
then
x . i in sum (F . i)
by A9, A10, GROUP_19:8;
hence
x . i in (sum_bundle F) . i
by Def7;
verum
end;
set SBF = sum_bundle F;
A11:
dom x = I
by GROUP_19:3;
reconsider W = Carrier (sum_bundle F) as ManySortedSet of I ;
A12:
dom W = I
by PARTFUN1:def 2;
for i being object st i in I holds
x . i in W . i
then
x in product W
by A11, A12, CARD_3:def 5;
then reconsider x = x as Element of (product (sum_bundle F)) by GROUP_7:def 2;
reconsider sry1 = (supp_restr (y,F)) | (support (x,(sum_bundle F))) as non-empty disjoint_valued ManySortedSet of support (x,(sum_bundle F)) by A4, A5, Th29;
Union sry1 is finite
by A3, A4, A5, Th29;
then
dom sry1 is finite
by Th30;
then
support (x,(sum_bundle F)) is finite
by PARTFUN1:def 2;
hence
( y = (dprod2prod F) . x & x in dsum F )
by A4, GROUP_19:8; verum