let I1, I2 be non empty set ; :: thesis:
let J1 be non-Empty TopSpace-yielding ManySortedSet of I1; :: thesis:
let J2 be non-Empty TopSpace-yielding ManySortedSet of I2; :: thesis:
let p be Function of I1,I2; :: thesis:
let H be ProductHomeo of J1,J2,p; :: thesis:
assume that
A1: p is bijective and
A2: for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ; :: thesis:
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;
A5: H is bijective by A1, A2, Th77;
ex K being prebasis of (product J1) ex L being prebasis of (product J2) st H .: K = L

reconsider K = product_prebasis J1 as prebasis of (product J1) by WAYBEL18:def 3;
reconsider L = product_prebasis J2 as prebasis of (product J2) by WAYBEL18:def 3;
take K ; :: thesis:
take L ; :: thesis:
for W being Subset of (product J2) holds
( W in L iff ex V being Subset of (product J1) st
( V in K & H .: V = W ) )

let W be Subset of (product J2); :: thesis:
thus ( W in L implies ex V being Subset of (product J1) st
( V in K & H .: V = W ) ) :: thesis:

assume W in L ; :: thesis:
then consider j being set , T being TopStruct , W0j being Subset of T such that
A6: ( j in I2 & W0j is open & T = J2 . j ) and
A7: W = product ((Carrier J2) +* (j,W0j)) by WAYBEL18:def 2;
reconsider j = j as Element of I2 by A6;
reconsider Wj = W0j as Subset of (J2 . j) by A6;
j in I2 ;
then j in rng p by A1, FUNCT_2:def 3;
then consider i being object such that
A8: ( i in I1 & p . i = j ) by FUNCT_2:11;
A9: i in dom p by A8, FUNCT_2:def 1;
reconsider i = i as Element of I1 by A8;
consider f being Function of (J1 . i),((J2 * p) . i) such that
A10: ( F . i = f & f is being_homeomorphism ) by A3;
reconsider Vi = f " Wj as Subset of (J1 . i) ;
A11: the carrier of (J1 . i) = [#] (J1 . i) by STRUCT_0:def 3
.= (Carrier J1) . i by PENCIL_3:7 ;
i in dom (Carrier J1) by A8, PARTFUN1:def 2;
then product ((Carrier J1) +* (i,Vi)) c= product (Carrier J1) by A11, Th39;
then reconsider V = product ((Carrier J1) +* (i,Vi)) as Subset of (product J1) by WAYBEL18:def 3;
take V ; :: thesis:
A12: V is Subset of (product (Carrier J1)) by WAYBEL18:def 3;
ex k being set ex S being TopStruct ex U being Subset of S st
( k in I1 & U is open & S = J1 . k & V = product ((Carrier J1) +* (k,U)) )

take i ; :: thesis:
take J1 . i ; :: thesis:
take Vi ; :: thesis:
reconsider W1j = Wj as Subset of ((J2 * p) . i) by A8, A9, FUNCT_1:13;
W0j in the topology of (J2 . j) by A6, PRE_TOPC:def 2;
then W1j in the topology of ((J2 * p) . i) by A8, A9, FUNCT_1:13;
then A14: W1j is open by PRE_TOPC:def 2;
( [#] ((J2 * p) . i) = {} implies [#] (J1 . i) = {} ) ;
hence ( i in I1 & Vi is open & J1 . i = J1 . i & V = product ((Carrier J1) +* (i,Vi)) ) by A10, A14, TOPS_2:43; :: thesis:

end;

hence V in K by A12, WAYBEL18:def 2; :: thesis:
reconsider f0 = f as one-to-one Function by A10;
rng f0 = [#] ((J2 * p) . i) by A10, TOPS_2:def 5
.= [#] (J2 . j) by A9, A8, FUNCT_1:13
.= the carrier of (J2 . j) by STRUCT_0:def 3 ;
then f .: (f " Wj) = Wj by FUNCT_1:77;
hence H .: V = W by A1, A3, A4, A7, A8, Th76, A10; :: thesis:

end;

given V being Subset of (product J1) such that A16: ( V in K & H .: V = W ) ; :: thesis:
consider i being set , S being TopStruct , Vi being Subset of S such that
A17: ( i in I1 & Vi is open & S = J1 . i ) and
A18: V = product ((Carrier J1) +* (i,Vi)) by A16, WAYBEL18:def 2;
reconsider i = i as Element of I1 by A17;
reconsider Vi = Vi as Subset of (J1 . i) by A17;
A19: W is Subset of (product (Carrier J2)) by WAYBEL18:def 3;
ex j being set ex T being TopStruct ex U being Subset of T st
( j in I2 & U is open & T = J2 . j & W = product ((Carrier J2) +* (j,U)) )

reconsider j = p . i as Element of I2 ;
consider f being Function of (J1 . i),((J2 * p) . i) such that
A20: ( F . i = f & f is being_homeomorphism ) by A3;
a21: i in dom p by A17, FUNCT_2:def 1;
then A21: (J2 * p) . i = J2 . j by FUNCT_1:13;
reconsider Wj = f .: Vi as Subset of (J2 . j) by a21, FUNCT_1:13;
take j ; :: thesis:
take J2 . j ; :: thesis:
take Wj ; :: thesis:
thus ( j in I2 & Wj is open & J2 . j = J2 . j ) by A21, A17, A20, T_0TOPSP:def 2; :: thesis:
thus W = product ((Carrier J2) +* (j,Wj)) by A16, A1, A3, A4, A18, A20, Th76; :: thesis:

end;

end;

end;