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 y being Element of (product (Union F))
for i being Element of I holds y | (J . i) in product (F . i)
let J be non-empty disjoint_valued ManySortedSet of I; for F being Group-Family of I,J
for y being Element of (product (Union F))
for i being Element of I holds y | (J . i) in product (F . i)
let F be Group-Family of I,J; for y being Element of (product (Union F))
for i being Element of I holds y | (J . i) in product (F . i)
let y be Element of (product (Union F)); for i being Element of I holds y | (J . i) in product (F . i)
let i be Element of I; y | (J . i) in product (F . i)
set x = y | (J . i);
A1:
dom J = I
by PARTFUN1:def 2;
A2:
dom (Union F) = Union J
by PARTFUN1:def 2;
A3:
dom y = Union J
by GROUP_19:3;
A4:
J . i c= Union J
by A1, FUNCT_1:3, ZFMISC_1:74;
then A5:
dom (y | (J . i)) = J . i
by A3, RELAT_1:62;
set z = Carrier (F . i);
A6:
dom (Carrier (F . i)) = J . i
by PARTFUN1:def 2;
for j being object st j in J . i holds
(y | (J . i)) . j in (Carrier (F . i)) . j
proof
let j be
object ;
( j in J . i implies (y | (J . i)) . j in (Carrier (F . i)) . j )
assume
j in J . i
;
(y | (J . i)) . j in (Carrier (F . i)) . j
then reconsider j =
j as
Element of
J . i ;
reconsider j1 =
j as
Element of
Union J by A4;
reconsider D =
Union F as
Group-Family of
Union J ;
y in product (Union F)
;
then A8:
y . j1 in D . j1
by GROUP_19:5;
A9:
(y | (J . i)) . j = y . j
by FUNCT_1:49;
[j,((Union F) . j)] in Union F
by A2, A4, FUNCT_1:1;
then consider Y0 being
set such that A10:
(
[j,((Union F) . j)] in Y0 &
Y0 in rng F )
by TARSKI:def 4;
consider k being
object such that A11:
(
k in dom F &
Y0 = F . k )
by A10, FUNCT_1:def 3;
reconsider k =
k as
Element of
I by A11;
reconsider Fk =
F . k as
Function ;
A12:
dom Fk = J . k
by PARTFUN1:def 2;
j in dom Fk
by A10, A11, XTUPLE_0:def 12;
then A13:
(J . k) /\ (J . i) <> {}
by A12, XBOOLE_0:def 4;
A14:
i = k
by A13, PROB_2:def 2, XBOOLE_0:def 7;
reconsider T =
(F . i) . j as
Group ;
(Carrier (F . i)) . j = [#] T
by PENCIL_3:7;
hence
(y | (J . i)) . j in (Carrier (F . i)) . j
by A8, A9, A10, A11, A14, FUNCT_1:1;
verum
end;
then
y | (J . i) in product (Carrier (F . i))
by A5, A6, CARD_3:def 5;
hence
y | (J . i) in product (F . i)
by GROUP_7:def 2; verum