end;

end;

assume {} in rng f ; :: thesis:
then consider i being object such that
A6: ( i in dom f & {} = f . i ) by FUNCT_1:def 3;
i in support (z,(sum_bundle F)) by A6;
then reconsider i = i as Element of I ;
A7: {} = (supp_restr (x,F)) . i by A6, FUNCT_1:47;
A8: support ((x | (J . i)),(F . i)) = {} by A7, Def12;
ex Z being Group st
( Z = (sum_bundle F) . i & z . i <> 1_ Z & i in I ) by A6, GROUP_19:def 1;
then A9: z . i <> 1_ (sum (F . i)) by Def7;
z . i in (prod_bundle F) . i by A1, GROUP_19:5;
then A10: z . i in product (F . i) by Def6;
then reconsider zi = z . i as Function ;
ex j being Element of J . i st zi . j <> 1_ ((F . i) . j)

assume A11: for j being Element of J . i holds zi . j = 1_ ((F . i) . j) ; :: thesis:
dom zi = J . i by A10, GROUP_19:3;
then reconsider zi = zi as ManySortedSet of J . i by PARTFUN1:def 2, RELAT_1:def 18;
for k being set st k in J . i holds
ex G being non empty Group-like multMagma st
( G = (F . i) . k & zi . k = 1_ G )

let k be set ; :: thesis:
assume k in J . i ; :: thesis:
then reconsider j = k as Element of J . i ;
take G = (F . i) . j; :: thesis:
thus G = (F . i) . k ; :: thesis:
thus zi . k = 1_ G by A11; :: thesis:

end;

end;

then consider j being Element of J . i such that
A12: zi . j <> 1_ ((F . i) . j) ;
j in support (zi,(F . i)) by A12, GROUP_19:def 1;
hence contradiction by A1, A2, A8, Def10; :: thesis:

end;

let k be object ; :: thesis:
assume k in support (x,(Union F)) ; :: thesis:
then consider Y being set such that
A15: ( k in Y & Y in rng (supp_restr (x,F)) ) by A13, TARSKI:def 4;
consider i being object such that
A16: ( i in dom (supp_restr (x,F)) & Y = (supp_restr (x,F)) . i ) by A15, FUNCT_1:def 3;
reconsider i = i as Element of I by A16;
k in support ((x | (J . i)),(F . i)) by A15, A16, Def12;
then consider Z being Group such that
A17: ( Z = (F . i) . k & (x | (J . i)) . k <> 1_ Z & k in J . i ) by GROUP_19:def 1;
z . i in (prod_bundle F) . i by A1, GROUP_19:5;
then A18: z . i in product (F . i) by Def6;
then reconsider zi = z . i as Function ;
dom zi = J . i by A18, GROUP_19:3;
then reconsider zi = zi as ManySortedSet of J . i by PARTFUN1:def 2, RELAT_1:def 18;
A19: ( zi . k <> 1_ Z & k in J . i ) by A1, A2, A17, Def10;
zi <> 1_ (product (F . i)) by A17, A19, GROUP_7:6;
then z . i <> 1_ (sum (F . i)) by GROUP_2:44;
then z . i <> 1_ ((sum_bundle F) . i) by Def7;
then i in support (z,(sum_bundle F)) by GROUP_19:def 1;
then A20: i in dom ((supp_restr (x,F)) | (support (z,(sum_bundle F)))) by A16, RELAT_1:57;
then Y = ((supp_restr (x,F)) | (support (z,(sum_bundle F)))) . i by A16, FUNCT_1:47;
then Y in rng ((supp_restr (x,F)) | (support (z,(sum_bundle F)))) by A20, FUNCT_1:3;
hence k in Union ((supp_restr (x,F)) | (support (z,(sum_bundle F)))) by A15, TARSKI:def 4; :: thesis:

end;