A1:
dom J = I
by PARTFUN1:def 2;
defpred S1[ Function, Function] means for i being Element of I holds $1 . i = $2 | (J . i);
A2:
for x being Element of (dprod F) ex y being Element of (product (Union F)) st S1[x,y]
proof
let x be
Element of
(dprod F);
ex y being Element of (product (Union F)) st S1[x,y]
A3:
x in product (prod_bundle F)
;
A4:
dom x = I
by GROUP_19:3;
A5:
for
i being
Element of
I holds
x . i in product (F . i)
set y =
Union x;
for
z being
object st
z in Union x holds
ex
a,
b being
object st
z = [a,b]
proof
let z be
object ;
( z in Union x implies ex a, b being object st z = [a,b] )
assume
z in Union x
;
ex a, b being object st z = [a,b]
then consider Y being
set such that A6:
(
z in Y &
Y in rng x )
by TARSKI:def 4;
consider i being
object such that A7:
(
i in dom x &
Y = x . i )
by A6, FUNCT_1:def 3;
reconsider i =
i as
Element of
I by A7, GROUP_19:3;
x . i in product (F . i)
by A5;
hence
ex
a,
b being
object st
z = [a,b]
by A6, A7, RELAT_1:def 1;
verum
end;
then
Union x is
Relation-like
;
then reconsider y =
Union x as
Relation ;
for
a,
b1,
b2 being
object st
[a,b1] in y &
[a,b2] in y holds
b1 = b2
proof
let a,
b1,
b2 be
object ;
( [a,b1] in y & [a,b2] in y implies b1 = b2 )
assume A8:
(
[a,b1] in y &
[a,b2] in y )
;
b1 = b2
then consider Y1 being
set such that A9:
(
[a,b1] in Y1 &
Y1 in rng x )
by TARSKI:def 4;
consider i1 being
object such that A10:
(
i1 in dom x &
Y1 = x . i1 )
by A9, FUNCT_1:def 3;
reconsider i1 =
i1 as
Element of
I by A10, GROUP_19:3;
A11:
x . i1 in product (F . i1)
by A5;
reconsider xi1 =
x . i1 as
Function by A11;
A12:
a in dom xi1
by A9, A10, FUNCT_1:1;
A13:
a in J . i1
by A11, A12, GROUP_19:3;
consider Y2 being
set such that A14:
(
[a,b2] in Y2 &
Y2 in rng x )
by A8, TARSKI:def 4;
consider i2 being
object such that A15:
(
i2 in dom x &
Y2 = x . i2 )
by A14, FUNCT_1:def 3;
reconsider i2 =
i2 as
Element of
I by A15, GROUP_19:3;
A16:
x . i2 in product (F . i2)
by A5;
reconsider xi2 =
x . i2 as
Function by A16;
A17:
a in dom xi2
by A14, A15, FUNCT_1:1;
a in J . i2
by A16, A17, GROUP_19:3;
then A18:
(J . i1) /\ (J . i2) <> {}
by A13, XBOOLE_0:def 4;
i1 = i2
by A18, PROB_2:def 2, XBOOLE_0:def 7;
hence
b1 = b2
by A9, A10, A11, A14, A15, FUNCT_1:def 1;
verum
end;
then
y is
Function-like
;
then reconsider y =
y as
Function ;
A19:
for
a being
object holds
(
a in dom y iff
a in Union J )
proof
let a be
object ;
( a in dom y iff a in Union J )
hereby ( a in Union J implies a in dom y )
assume
a in dom y
;
a in Union Jthen consider b being
object such that A20:
[a,b] in y
by XTUPLE_0:def 12;
consider Y being
set such that A21:
(
[a,b] in Y &
Y in rng x )
by A20, TARSKI:def 4;
consider i being
object such that A22:
(
i in dom x &
Y = x . i )
by A21, FUNCT_1:def 3;
reconsider i =
i as
Element of
I by A22, GROUP_19:3;
A23:
x . i in product (F . i)
by A5;
then reconsider xi =
x . i as
Function ;
A24:
a in dom xi
by A21, A22, FUNCT_1:1;
(
a in J . i &
J . i in rng J )
by A1, A23, A24, FUNCT_1:3, GROUP_19:3;
hence
a in Union J
by TARSKI:def 4;
verum
end;
assume
a in Union J
;
a in dom y
then consider Y being
set such that A25:
(
a in Y &
Y in rng J )
by TARSKI:def 4;
consider i being
object such that A26:
(
i in dom J &
Y = J . i )
by A25, FUNCT_1:def 3;
reconsider i =
i as
Element of
I by A26;
A27:
x . i in product (F . i)
by A5;
reconsider xi =
x . i as
Function by A27;
a in dom xi
by A25, A26, A27, GROUP_19:3;
then consider b being
object such that A28:
[a,b] in xi
by XTUPLE_0:def 12;
xi in rng x
by A4, FUNCT_1:3;
then
[a,b] in y
by A28, TARSKI:def 4;
hence
a in dom y
by XTUPLE_0:def 12;
verum
end;
then A29:
dom y = Union J
by TARSKI:2;
then reconsider y =
y as
ManySortedSet of
Union J by PARTFUN1:def 2, RELAT_1:def 18;
reconsider z =
Carrier (Union F) as
ManySortedSet of
Union J ;
A30:
dom z = Union J
by PARTFUN1:def 2;
for
i being
object st
i in Union J holds
y . i in z . i
proof
let i be
object ;
( i in Union J implies y . i in z . i )
assume
i in Union J
;
y . i in z . i
then reconsider i =
i as
Element of
Union J ;
[i,(y . i)] in y
by A19, FUNCT_1:1;
then consider Yi being
set such that A31:
(
[i,(y . i)] in Yi &
Yi in rng x )
by TARSKI:def 4;
consider j being
object such that A32:
(
j in dom x &
Yi = x . j )
by A31, FUNCT_1:def 3;
reconsider j =
j as
Element of
I by A32, GROUP_19:3;
A33:
x . j in product (F . j)
by A5;
reconsider xj =
x . j as
Function by A33;
A34:
(
i in dom xj &
y . i = xj . i )
by A31, A32, FUNCT_1:1;
A35:
i in J . j
by A33, A34, GROUP_19:3;
dom (Union F) = Union J
by PARTFUN1:def 2;
then
[i,((Union F) . i)] in Union F
by FUNCT_1:1;
then consider Y0 being
set such that A36:
(
[i,((Union F) . i)] in Y0 &
Y0 in rng F )
by TARSKI:def 4;
consider k being
object such that A37:
(
k in dom F &
Y0 = F . k )
by A36, FUNCT_1:def 3;
reconsider k =
k as
Element of
I by A37;
reconsider Fk =
F . k as
Function ;
A38:
dom Fk = J . k
by PARTFUN1:def 2;
i in dom Fk
by A36, A37, XTUPLE_0:def 12;
then A39:
(J . k) /\ (J . j) <> {}
by A35, A38, XBOOLE_0:def 4;
reconsider P =
(F . j) . i as
Group by A35, GROUP_19:1;
j = k
by A39, PROB_2:def 2, XBOOLE_0:def 7;
then A40:
[#] P = [#] ((Union F) . i)
by A36, A37, FUNCT_1:1;
xj . i in P
by A33, A35, GROUP_19:5;
hence
y . i in z . i
by A34, A40, PENCIL_3:7;
verum
end;
then
y in product z
by A29, A30, CARD_3:def 5;
then reconsider y =
y as
Element of
(product (Union F)) by GROUP_7:def 2;
take
y
;
S1[x,y]
thus
for
i being
Element of
I holds
x . i = y | (J . i)
verumproof
let i be
Element of
I;
x . i = y | (J . i)
A41:
J . i c= Union J
by A1, FUNCT_1:3, ZFMISC_1:74;
then A42:
dom (y | (J . i)) = J . i
by A29, RELAT_1:62;
A43:
x . i in product (F . i)
by A5;
then reconsider xi =
x . i as
Function ;
for
j being
object st
j in dom xi holds
xi . j = (y | (J . i)) . j
proof
let j be
object ;
( j in dom xi implies xi . j = (y | (J . i)) . j )
assume
j in dom xi
;
xi . j = (y | (J . i)) . j
then A44:
j in J . i
by A43, GROUP_19:3;
then A45:
(y | (J . i)) . j = y . j
by FUNCT_1:49;
j in dom (y | (J . i))
by A29, A41, A44, RELAT_1:62;
then
j in (dom y) /\ (J . i)
by RELAT_1:61;
then
j in dom y
by XBOOLE_0:def 4;
then
[j,(y . j)] in y
by FUNCT_1:1;
then consider Y0 being
set such that A46:
(
[j,(y . j)] in Y0 &
Y0 in rng x )
by TARSKI:def 4;
consider k being
object such that A47:
(
k in dom x &
Y0 = x . k )
by A46, FUNCT_1:def 3;
reconsider k =
k as
Element of
I by A47, GROUP_19:3;
A48:
x . k in product (F . k)
by A5;
then reconsider xk =
x . k as
Function ;
A49:
dom xk = J . k
by A48, GROUP_19:3;
j in dom xk
by A46, A47, XTUPLE_0:def 12;
then A50:
(J . k) /\ (J . i) <> {}
by A44, A49, XBOOLE_0:def 4;
i = k
by A50, PROB_2:def 2, XBOOLE_0:def 7;
hence
xi . j = (y | (J . i)) . j
by A45, A46, A47, FUNCT_1:1;
verum
end;
hence
x . i = y | (J . i)
by A42, A43, FUNCT_1:2, GROUP_19:3;
verum
end;
end;
consider f being Function of (dprod F),(product (Union F)) such that
A51:
for x being Element of (dprod F) holds S1[x,f . x]
from FUNCT_2:sch 3(A2);
for a, b being Element of (dprod F) holds f . (a * b) = (f . a) * (f . b)
proof
let a,
b be
Element of
(dprod F);
f . (a * b) = (f . a) * (f . b)
reconsider fa =
f . a as
Element of
(product (Union F)) ;
reconsider fb =
f . b as
Element of
(product (Union F)) ;
set fafb =
fa * fb;
reconsider fab =
f . (a * b) as
Element of
(product (Union F)) ;
A52:
(
a in product (prod_bundle F) &
b in product (prod_bundle F) &
a * b in product (prod_bundle F) )
;
A53:
for
i being
Element of
I holds
(
a . i in product (F . i) &
b . i in product (F . i) &
(a * b) . i in product (F . i) )
A54:
dom fab = Union J
by GROUP_19:3;
for
j being
object st
j in dom fab holds
fab . j = (fa * fb) . j
proof
let j be
object ;
( j in dom fab implies fab . j = (fa * fb) . j )
assume A55:
j in dom fab
;
fab . j = (fa * fb) . j
then consider Y being
set such that A56:
(
j in Y &
Y in rng J )
by A54, TARSKI:def 4;
consider i being
object such that A57:
(
i in dom J &
Y = J . i )
by A56, FUNCT_1:def 3;
reconsider i =
i as
Element of
I by A57;
A58:
a . i = (f . a) | (J . i)
by A51;
A59:
b . i = (f . b) | (J . i)
by A51;
(
a . i in product (F . i) &
b . i in product (F . i) &
(a * b) . i in product (F . i) )
by A53;
then reconsider ai =
a . i,
bi =
b . i,
abi =
(a * b) . i as
Element of
(product (F . i)) ;
reconsider P =
(F . i) . j as
Group by A56, A57, GROUP_19:1;
ai . j in P
by A53, A56, A57, GROUP_19:5;
then reconsider aij =
ai . j as
Element of
P ;
bi . j in P
by A53, A56, A57, GROUP_19:5;
then reconsider bij =
bi . j as
Element of
P ;
A60:
aij = fa . j
by A56, A57, A58, FUNCT_1:49;
then reconsider faj =
fa . j as
Element of
P ;
bij = fb . j
by A56, A57, A59, FUNCT_1:49;
then reconsider fbj =
fb . j as
Element of
P ;
(prod_bundle F) . i = product (F . i)
by Def6;
then A61:
abi . j =
(ai * bi) . j
by GROUP_7:1
.=
aij * bij
by A56, A57, GROUP_7:1
;
A62:
j in Union J
by A55, GROUP_19:3;
dom (Union F) = Union J
by PARTFUN1:def 2;
then
[j,((Union F) . j)] in Union F
by A62, FUNCT_1:1;
then consider Y0 being
set such that A63:
(
[j,((Union F) . j)] in Y0 &
Y0 in rng F )
by TARSKI:def 4;
consider k being
object such that A64:
(
k in dom F &
Y0 = F . k )
by A63, FUNCT_1:def 3;
reconsider k =
k as
Element of
I by A64;
reconsider Fk =
F . k as
Function ;
j in dom Fk
by A63, A64, XTUPLE_0:def 12;
then
j in J . k
by PARTFUN1:def 2;
then A65:
(J . k) /\ (J . i) <> {}
by A56, A57, XBOOLE_0:def 4;
i = k
by A65, PROB_2:def 2, XBOOLE_0:def 7;
then A66:
(Union F) . j = (F . i) . j
by A63, A64, FUNCT_1:1;
thus fab . j =
((f . (a * b)) | (J . i)) . j
by A56, A57, FUNCT_1:49
.=
aij * bij
by A51, A61
.=
faj * fbj
by A56, A57, A59, A60, FUNCT_1:49
.=
(fa * fb) . j
by A62, A66, GROUP_7:1
;
verum
end;
hence
f . (a * b) = (f . a) * (f . b)
by A54, GROUP_19:3;
verum
end;
then reconsider f = f as Homomorphism of (dprod F),(product (Union F)) by GROUP_6:def 6;
take
f
; for x being Element of (dprod F)
for i being Element of I holds x . i = (f . x) | (J . i)
thus
for x being Element of (dprod F)
for i being Element of I holds x . i = (f . x) | (J . i)
by A51; verum