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

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

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

then A13:
H is one-to-one
by FUNCT_1:def 4;
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

end;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

hence
x1 = x2
by A7, FUNCT_1:2; :: thesis: verum
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;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

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