let I be non empty set ; :: thesis: for J being disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for j being Element of I
for i being object st i in J . j holds
(Union F) . i = (F . j) . i
let J be disjoint_valued ManySortedSet of I; :: thesis: for F being Group-Family of I,J
for j being Element of I
for i being object st i in J . j holds
(Union F) . i = (F . j) . i
let F be Group-Family of I,J; :: thesis: for j being Element of I
for i being object st i in J . j holds
(Union F) . i = (F . j) . i
let j be Element of I; :: thesis: for i being object st i in J . j holds
(Union F) . i = (F . j) . i
let i be object ; :: thesis: ( i in J . j implies (Union F) . i = (F . j) . i )
assume A1: i in J . j ; :: thesis: (Union F) . i = (F . j) . i
dom J = I by PARTFUN1:def 2;
then A3: J . j c= Union J by FUNCT_1:3, ZFMISC_1:74;
dom (Union F) = Union J by PARTFUN1:def 2;
then [i,((Union F) . i)] in Union F by A1, A3, FUNCT_1:1;
then consider Y0 being set such that
A4: ( [i,((Union F) . i)] in Y0 & Y0 in rng F ) by TARSKI:def 4;
consider k being object such that
A5: ( k in dom F & Y0 = F . k ) by A4, FUNCT_1:def 3;
reconsider k = k as Element of I by A5;
reconsider Fk = F . k as Function ;
A6: dom Fk = J . k by PARTFUN1:def 2;
i in dom Fk by A4, A5, XTUPLE_0:def 12;
then (J . k) /\ (J . j) <> {} by A1, A6, XBOOLE_0:def 4;
then j = k by PROB_2:def 2, XBOOLE_0:def 7;
hence (Union F) . i = (F . j) . i by A4, A5, FUNCT_1:1; :: thesis: verum