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 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; :: thesis: 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; :: thesis: 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)); :: thesis: for i being Element of I holds y | (J . i) in product (F . i)
let i be Element of I; :: thesis: 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 ; :: thesis: ( j in J . i implies (y | (J . i)) . j in (Carrier (F . i)) . j )
assume j in J . i ; :: thesis: (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; :: thesis: 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; :: thesis: verum