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 x being Function holds support (x,(Union F)) = Union (supp_restr (x,F))
let J be non-empty disjoint_valued ManySortedSet of I; :: thesis: for F being Group-Family of I,J
for x being Function holds support (x,(Union F)) = Union (supp_restr (x,F))
let F be Group-Family of I,J; :: thesis: for x being Function holds support (x,(Union F)) = Union (supp_restr (x,F))
let x be Function; :: thesis: support (x,(Union F)) = Union (supp_restr (x,F))
set y = supp_restr (x,F);
A1: dom J = I by PARTFUN1:def 2;
A2: dom (supp_restr (x,F)) = I by PARTFUN1:def 2;
for j being object holds
( j in support (x,(Union F)) iff j in Union (supp_restr (x,F)) )

proof

let j be object ; :: thesis: ( j in support (x,(Union F)) iff j in Union (supp_restr (x,F)) )

hereby :: thesis: ( j in Union (supp_restr (x,F)) implies j in support (x,(Union F)) )

assume j in support (x,(Union F)) ; :: thesis: j in Union (supp_restr (x,F))
then A3: ( x . j <> 1_ ((Union F) . j) & j in Union J ) by GROUP_19:def 1;
then j in union (rng J) by CARD_3:def 4;
then consider Y being set such that
A4: ( j in Y & Y in rng J ) by TARSKI:def 4;
consider i being object such that
A5: ( i in dom J & Y = J . i ) by A4, FUNCT_1:def 3;
reconsider i = i as Element of I by A5;
reconsider j0 = j as Element of J . i by A4, A5;
(F . i) . j0 = (Union F) . j0 by Th19;
then (x | (J . i)) . j <> 1_ ((F . i) . j) by A3, FUNCT_1:49;
then j in support ((x | (J . i)),(F . i)) by A4, A5, GROUP_19:def 1;
then A6: j in (supp_restr (x,F)) . i by Def12;
(supp_restr (x,F)) . i in rng (supp_restr (x,F)) by A2, FUNCT_1:3;
then j in union (rng (supp_restr (x,F))) by A6, TARSKI:def 4;
hence j in Union (supp_restr (x,F)) by CARD_3:def 4; :: thesis: verum

end;

assume j in Union (supp_restr (x,F)) ; :: thesis: j in support (x,(Union F))
then j in union (rng (supp_restr (x,F))) by CARD_3:def 4;
then consider Y being set such that
A7: ( j in Y & Y in rng (supp_restr (x,F)) ) by TARSKI:def 4;
consider i being object such that
A8: ( i in dom (supp_restr (x,F)) & Y = (supp_restr (x,F)) . i ) by A7, FUNCT_1:def 3;
reconsider i = i as Element of I by A8;
A9: (supp_restr (x,F)) . i = support ((x | (J . i)),(F . i)) by Def12;
then A10: ( (x | (J . i)) . j <> 1_ ((F . i) . j) & j in J . i ) by A7, A8, GROUP_19:def 1;
A11: (x | (J . i)) . j = x . j by A7, A8, A9, FUNCT_1:49;
A12: 1_ ((F . i) . j) = 1_ ((Union F) . j) by A7, A8, A9, Th19;
J . i c= union (rng J) by A1, FUNCT_1:3, ZFMISC_1:74;
then J . i c= Union J by CARD_3:def 4;
hence j in support (x,(Union F)) by A10, A11, A12, GROUP_19:def 1; :: thesis: verum

end;

hence support (x,(Union F)) = Union (supp_restr (x,F)) by TARSKI:2; :: thesis: verum