let H1, H2 be Homomorphism of (dprod F),(product (Union F)); :: thesis: ( ( for x being Element of (dprod F)
for i being Element of I holds x . i = (H1 . x) | (J . i) ) & ( for x being Element of (dprod F)
for i being Element of I holds x . i = (H2 . x) | (J . i) ) implies H1 = H2 )
assume that
A67: for x being Element of (dprod F)
for i being Element of I holds x . i = (H1 . x) | (J . i) and
A68: for x being Element of (dprod F)
for i being Element of I holds x . i = (H2 . x) | (J . i) ; :: thesis: H1 = H2
for x being Element of (dprod F) holds H1 . x = H2 . x

proof

let x be Element of (dprod F); :: thesis: H1 . x = H2 . x
A69: x in product (prod_bundle F) ;
A70: for i being Element of I holds x . i in product (F . i)

proof

let i be Element of I; :: thesis: x . i in product (F . i)
x . i in (prod_bundle F) . i by A69, GROUP_19:5;
hence x . i in product (F . i) by Def6; :: thesis: verum

end;

reconsider H1x = H1 . x, H2x = H2 . x as Function ;
A71: dom H1x = Union J by GROUP_19:3;
for j being object st j in dom H1x holds
H1x . j = H2x . j

proof

let j be object ; :: thesis: ( j in dom H1x implies H1x . j = H2x . j )
assume j in dom H1x ; :: thesis: H1x . j = H2x . j
then consider Y being set such that
A72: ( j in Y & Y in rng J ) by A71, TARSKI:def 4;
consider i being object such that
A73: ( i in dom J & Y = J . i ) by A72, FUNCT_1:def 3;
reconsider i = i as Element of I by A73;
x . i in product (F . i) by A70;
then reconsider xi = x . i as Function ;
thus H1x . j = (H1x | (J . i)) . j by A72, A73, FUNCT_1:49
.= xi . j by A67
.= (H2x | (J . i)) . j by A68
.= H2x . j by A72, A73, FUNCT_1:49 ; :: thesis: verum

end;

hence H1 . x = H2 . x by A71, GROUP_19:3; :: thesis: verum

end;

hence H1 = H2 by FUNCT_2:63; :: thesis: verum