let I1, I2 be non empty set ; :: thesis: for J1 being non-Empty TopSpace-yielding ManySortedSet of I1
for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
H is bijective
let J1 be non-Empty TopSpace-yielding ManySortedSet of I1; :: thesis: for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
H is bijective
let J2 be non-Empty TopSpace-yielding ManySortedSet of I2; :: thesis: for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
H is bijective
let p be Function of I1,I2; :: thesis: for H being ProductHomeo of J1,J2,p st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
H is bijective
let H be ProductHomeo of J1,J2,p; :: thesis: ( p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) implies H is bijective )
assume that
A1: p is bijective and
A2: for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ; :: thesis: H is bijective
consider F being ManySortedFunction of I1 such that
A3: for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) and
A4: for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) by A1, A2, Def5;
for x1, x2 being object st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 )
assume A5: ( x1 in dom H & x2 in dom H & H . x1 = H . x2 ) ; :: thesis: x1 = x2
then reconsider g1 = x1, g2 = x2 as Element of (product J1) ;
A6: ( g1 is Element of product (Carrier J1) & g2 is Element of product (Carrier J1) ) by WAYBEL18:def 3;
A7: dom g1 = dom (Carrier J1) by A6, CARD_3:9
.= dom g2 by A6, CARD_3:9 ;
for z being object st z in dom g1 holds
g1 . z = g2 . z

proof

let z be object ; :: thesis: ( z in dom g1 implies g1 . z = g2 . z )
assume z in dom g1 ; :: thesis: g1 . z = g2 . z
then z in dom (Carrier J1) by A6, CARD_3:9;
then reconsider i = z as Element of I1 ;
a8: ( (H . g1) . (p . i) = (F . i) . (g1 . i) & (H . g2) . (p . i) = (F . i) . (g2 . i) ) by A4;
consider f being Function of (J1 . i),((J2 * p) . i) such that
A9: ( F . i = f & f is being_homeomorphism ) by A3;
A12: (Carrier J1) . i = [#] (J1 . i) by PENCIL_3:7
.= the carrier of (J1 . i) by STRUCT_0:def 3
.= dom f by FUNCT_2:def 1 ;
i in I1 ;
then i in dom (Carrier J1) by PARTFUN1:def 2;
then ( g1 . i in (Carrier J1) . i & g2 . i in (Carrier J1) . i ) by A6, CARD_3:9;
hence g1 . z = g2 . z by a8, A5, A9, A12, FUNCT_1:def 4; :: thesis: verum

end;

hence x1 = x2 by A7, FUNCT_1:2; :: thesis: verum

end;

then A13: H is one-to-one by FUNCT_1:def 4;
set i0 = the Element of I1;
consider f0 being Function of (J1 . the Element of I1),((J2 * p) . the Element of I1) such that
A14: ( F . the Element of I1 = f0 & f0 is being_homeomorphism ) by A3;
the Element of I1 in I1 ;
then A15: the Element of I1 in dom p by FUNCT_2:def 1;
rng H = H .: (dom H) by RELAT_1:113
.= H .: the carrier of (product J1) by FUNCT_2:def 1
.= H .: (product (Carrier J1)) by WAYBEL18:def 3
.= H .: (product ((Carrier J1) +* ( the Element of I1,((Carrier J1) . the Element of I1)))) by FUNCT_7:35
.= H .: (product ((Carrier J1) +* ( the Element of I1,([#] (J1 . the Element of I1))))) by PENCIL_3:7
.= product ((Carrier J2) +* ((p . the Element of I1),((F . the Element of I1) .: ([#] (J1 . the Element of I1))))) by A1, A3, A4, Th76
.= product ((Carrier J2) +* ((p . the Element of I1),(f0 .: (dom f0)))) by A14, TOPS_2:def 5
.= product ((Carrier J2) +* ((p . the Element of I1),(rng f0))) by RELAT_1:113
.= product ((Carrier J2) +* ((p . the Element of I1),([#] ((J2 * p) . the Element of I1)))) by A14, TOPS_2:def 5
.= product ((Carrier J2) +* ((p . the Element of I1),([#] (J2 . (p . the Element of I1))))) by A15, FUNCT_1:13
.= product ((Carrier J2) +* ((p . the Element of I1),((Carrier J2) . (p . the Element of I1)))) by PENCIL_3:7
.= product (Carrier J2) by FUNCT_7:35
.= the carrier of (product J2) by WAYBEL18:def 3 ;
then H is onto by FUNCT_2:def 3;
hence H is bijective by A13; :: thesis: verum