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 holds dprod2prod F is bijective
let J be non-empty disjoint_valued ManySortedSet of I; :: thesis: for F being Group-Family of I,J holds dprod2prod F is bijective
let F be Group-Family of I,J; :: thesis: dprod2prod F is bijective
set f = dprod2prod F;
for x1, x2 being object st x1 in dom (dprod2prod F) & x2 in dom (dprod2prod F) & (dprod2prod F) . x1 = (dprod2prod F) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom (dprod2prod F) & x2 in dom (dprod2prod F) & (dprod2prod F) . x1 = (dprod2prod F) . x2 implies x1 = x2 )
assume that
A1: x1 in dom (dprod2prod F) and
A2: x2 in dom (dprod2prod F) and
A3: (dprod2prod F) . x1 = (dprod2prod F) . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of (dprod F) by A1, A2;
A4: dom x1 = I by GROUP_19:3;
for i being object st i in dom x1 holds
x1 . i = x2 . i

proof

let i be object ; :: thesis: ( i in dom x1 implies x1 . i = x2 . i )
assume i in dom x1 ; :: thesis: x1 . i = x2 . i
then reconsider i = i as Element of I by GROUP_19:3;
x1 . i = ((dprod2prod F) . x2) | (J . i) by A3, Def10
.= x2 . i by Def10 ;
hence x1 . i = x2 . i ; :: thesis: verum

end;

then x1 = x2 by A4, GROUP_19:3;
hence x1 = x2 ; :: thesis: verum

end;

hence dprod2prod F is one-to-one ; :: according to FUNCT_2:def 4 :: thesis: dprod2prod F is onto
for y being object st y in [#] (product (Union F)) holds
ex x being object st
( x in [#] (dprod F) & y = (dprod2prod F) . x )

proof

let y be object ; :: thesis: ( y in [#] (product (Union F)) implies ex x being object st
( x in [#] (dprod F) & y = (dprod2prod F) . x ) )
assume y in [#] (product (Union F)) ; :: thesis: ex x being object st
( x in [#] (dprod F) & y = (dprod2prod F) . x )
then reconsider y = y as Element of (product (Union F)) ;
deffunc H₁( object ) -> set = y | (J . $1);
consider x being Function such that
A5: ( dom x = I & ( for i being object st i in I holds
x . i = H₁(i) ) ) from FUNCT_1:sch 3();
reconsider x = x as ManySortedSet of I by A5, PARTFUN1:def 2, RELAT_1:def 18;
set z = Carrier (prod_bundle F);
A6: dom (Carrier (prod_bundle F)) = I by PARTFUN1:def 2;
for i being object st i in I holds
x . i in (Carrier (prod_bundle F)) . i

proof

let i be object ; :: thesis: ( i in I implies x . i in (Carrier (prod_bundle F)) . i )
assume i in I ; :: thesis: x . i in (Carrier (prod_bundle F)) . i
then reconsider i = i as Element of I ;
A7: (Carrier (prod_bundle F)) . i = [#] ((prod_bundle F) . i) by PENCIL_3:7
.= [#] (product (F . i)) by Def6 ;
y | (J . i) in product (F . i) by Th23;
hence x . i in (Carrier (prod_bundle F)) . i by A5, A7; :: thesis: verum

end;

then x in product (Carrier (prod_bundle F)) by A5, A6, CARD_3:def 5;
then reconsider x = x as Element of (dprod F) by GROUP_7:def 2;
take x ; :: thesis: ( x in [#] (dprod F) & y = (dprod2prod F) . x )
thus x in [#] (dprod F) ; :: thesis: y = (dprod2prod F) . x
A8: x in product (prod_bundle F) ;
A9: 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 A8, GROUP_19:5;
hence x . i in product (F . i) by Def6; :: thesis: verum

end;

reconsider H1x = y, H2x = (dprod2prod F) . x as Function ;
A10: 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
A11: ( j in Y & Y in rng J ) by A10, TARSKI:def 4;
consider i being object such that
A12: ( i in dom J & Y = J . i ) by A11, FUNCT_1:def 3;
reconsider i = i as Element of I by A12;
x . i in product (F . i) by A9;
then reconsider xi = x . i as Function ;
thus H1x . j = (H1x | (J . i)) . j by A11, A12, FUNCT_1:49
.= xi . j by A5
.= (H2x | (J . i)) . j by Def10
.= H2x . j by A11, A12, FUNCT_1:49 ; :: thesis: verum

end;

then y = (dprod2prod F) . x by A10, GROUP_19:3;
hence y = (dprod2prod F) . x ; :: thesis: verum

end;

then rng (dprod2prod F) = [#] (product (Union F)) by FUNCT_2:10;
hence dprod2prod F is onto by FUNCT_2:def 3; :: thesis: verum