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 being Function holds support (x,(Union F)) = Union (supp_restr (x,F))
let J be 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 F be Group-Family of I,J; for x being Function holds support (x,(Union F)) = Union (supp_restr (x,F))
let x be Function; 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 ;
( j in support (x,(Union F)) iff j in Union (supp_restr (x,F)) )
hereby ( j in Union (supp_restr (x,F)) implies j in support (x,(Union F)) )
assume
j in support (
x,
(Union F))
;
j in Union (supp_restr (x,F))then consider Z being
Group such that A3:
(
Z = (Union F) . j &
x . j <> 1_ Z &
j in Union J )
by GROUP_19:def 1;
consider Y being
set such that A4:
(
j in Y &
Y in rng J )
by A3, 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) . j0)
by A3, FUNCT_1:49;
then
j in support (
(x | (J . i)),
(F . i))
by 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;
hence
j in Union (supp_restr (x,F))
by A6, TARSKI:def 4;
verum
end;
assume
j in Union (supp_restr (x,F))
;
j in support (x,(Union F))
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 consider Z being
Group such that A10:
(
Z = (F . i) . j &
(x | (J . i)) . j <> 1_ Z &
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;
J . i in rng J
by A1, FUNCT_1:3;
then reconsider j0 =
j as
Element of
Union J by A10, TARSKI:def 4;
reconsider ZZ =
(Union F) . j0 as
Group ;
1_ Z = 1_ ZZ
by A10, Th19;
hence
j in support (
x,
(Union F))
by A10, A11, GROUP_19:def 1;
verum
end;
hence
support (x,(Union F)) = Union (supp_restr (x,F))
by TARSKI:2; verum