let I be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: 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
proof
let i be object ; :: thesis: ( i in I implies x . i in W . i )
assume i in I ; :: thesis: x . i in W . i
then reconsider i = i as Element of I ;
A13: W . i = [#] ((sum_bundle F) . i) by PENCIL_3:7;
x . i in (sum_bundle F) . i by A7;
hence x . i in W . i by A13; :: thesis: verum
end;
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; :: thesis: verum