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 x, y being Function st x in dsum F & x in dsum F holds
(dprod2prod F) . x in sum (Union F)
let J be non-empty disjoint_valued ManySortedSet of I; for F being Group-Family of I,J
for x, y being Function st x in dsum F & x in dsum F holds
(dprod2prod F) . x in sum (Union F)
let F be Group-Family of I,J; for x, y being Function st x in dsum F & x in dsum F holds
(dprod2prod F) . x in sum (Union F)
let x, y be Function; ( x in dsum F & x in dsum F implies (dprod2prod F) . x in sum (Union F) )
assume A1:
x in dsum F
; ( not x in dsum F or (dprod2prod F) . x in sum (Union F) )
then A2:
x in dprod F
by GROUP_2:40;
then reconsider y = (dprod2prod F) . x as Element of (product (Union F)) by FUNCT_2:5;
deffunc H1( object ) -> Element of bool (J . (In ($1,I))) = support ((y | (J . (In ($1,I)))),(F . (In ($1,I))));
set sry = supp_restr (y,F);
reconsider sry1 = (supp_restr (y,F)) | (support (x,(sum_bundle F))) as non-empty disjoint_valued ManySortedSet of support (x,(sum_bundle F)) by A2, Th29;
for i being object st i in dom sry1 holds
sry1 . i is finite
then
Union sry1 is finite
by A1, CARD_2:88;
then
support (y,(Union F)) is finite
by A2, Th29;
hence
( not x in dsum F or (dprod2prod F) . x in sum (Union F) )
by GROUP_19:8; verum