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

for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

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

for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

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

for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let p be Function of I1,I2; :: thesis: for H being ProductHomeo of J1,J2,p

for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let H be ProductHomeo of J1,J2,p; :: thesis: for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let F be ManySortedFunction of I1; :: thesis: ( p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) implies for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U))) )

assume that

A1: p is bijective and

A2: 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

A3: for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ; :: thesis: for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let i be Element of I1; :: thesis: for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let U be Subset of (J1 . i); :: thesis: H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

reconsider j = p . i as Element of I2 ;

i in I1 ;

then A4: i in dom p by FUNCT_2:def 1;

consider f being Function of (J1 . i),((J2 * p) . i) such that

A5: ( F . i = f & f is being_homeomorphism ) by A2;

A6: rng f = [#] ((J2 * p) . i) by A5, TOPS_2:def 5

.= [#] (J2 . j) by A4, FUNCT_1:13

.= the carrier of (J2 . j) by STRUCT_0:def 3 ;

for y being object holds

( y in H .: (product ((Carrier J1) +* (i,U))) iff y in product ((Carrier J2) +* (j,((F . i) .: U))) )

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

for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

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

for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

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

for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let p be Function of I1,I2; :: thesis: for H being ProductHomeo of J1,J2,p

for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let H be ProductHomeo of J1,J2,p; :: thesis: for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds

for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let F be ManySortedFunction of I1; :: thesis: ( p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st

( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) implies for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U))) )

assume that

A1: p is bijective and

A2: 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

A3: for g being Element of (product J1)

for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ; :: thesis: for i being Element of I1

for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let i be Element of I1; :: thesis: for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let U be Subset of (J1 . i); :: thesis: H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

reconsider j = p . i as Element of I2 ;

i in I1 ;

then A4: i in dom p by FUNCT_2:def 1;

consider f being Function of (J1 . i),((J2 * p) . i) such that

A5: ( F . i = f & f is being_homeomorphism ) by A2;

A6: rng f = [#] ((J2 * p) . i) by A5, TOPS_2:def 5

.= [#] (J2 . j) by A4, FUNCT_1:13

.= the carrier of (J2 . j) by STRUCT_0:def 3 ;

for y being object holds

( y in H .: (product ((Carrier J1) +* (i,U))) iff y in product ((Carrier J2) +* (j,((F . i) .: U))) )

proof

hence
H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
by TARSKI:2; :: thesis: verum
let y be object ; :: thesis: ( y in H .: (product ((Carrier J1) +* (i,U))) iff y in product ((Carrier J2) +* (j,((F . i) .: U))) )

thus ( y in H .: (product ((Carrier J1) +* (i,U))) implies y in product ((Carrier J2) +* (j,((F . i) .: U))) ) :: thesis: ( y in product ((Carrier J2) +* (j,((F . i) .: U))) implies y in H .: (product ((Carrier J1) +* (i,U))) )

then reconsider h = y as Element of product ((Carrier J2) +* (j,((F . i) .: U))) ;

A21: the carrier of (J1 . i) = [#] (J1 . i) by STRUCT_0:def 3

.= (Carrier J1) . i by PENCIL_3:7 ;

i in I1 ;

then A22: i in dom (Carrier J1) by PARTFUN1:def 2;

then A23: product ((Carrier J1) +* (i,U)) c= product (Carrier J1) by A21, Th39;

A24: (Carrier J2) . j = [#] (J2 . j) by PENCIL_3:7

.= the carrier of (J2 . j) by STRUCT_0:def 3 ;

a25: ( j in I2 & (F . i) .: U c= the carrier of (J2 . j) ) by A6, A5, RELAT_1:111;

then A25: ( j in dom (Carrier J2) & (F . i) .: U c= (Carrier J2) . j ) by A24, PARTFUN1:def 2;

then A26: product ((Carrier J2) +* (j,((F . i) .: U))) c= product (Carrier J2) by Th39;

ex x being object st

( x in dom H & x in product ((Carrier J1) +* (i,U)) & H . x = y )

end;thus ( y in H .: (product ((Carrier J1) +* (i,U))) implies y in product ((Carrier J2) +* (j,((F . i) .: U))) ) :: thesis: ( y in product ((Carrier J2) +* (j,((F . i) .: U))) implies y in H .: (product ((Carrier J1) +* (i,U))) )

proof

assume A20:
y in product ((Carrier J2) +* (j,((F . i) .: U)))
; :: thesis: y in H .: (product ((Carrier J1) +* (i,U)))
assume
y in H .: (product ((Carrier J1) +* (i,U)))
; :: thesis: y in product ((Carrier J2) +* (j,((F . i) .: U)))

then consider x being object such that

A8: ( x in dom H & x in product ((Carrier J1) +* (i,U)) & y = H . x ) by FUNCT_1:def 6;

reconsider g = x as Element of (product J1) by A8;

y in rng H by A8, FUNCT_1:3;

then reconsider h = y as Element of (product J2) ;

h in the carrier of (product J2) ;

then A9: h in product (Carrier J2) by WAYBEL18:def 3;

then A10: dom h = dom (Carrier J2) by CARD_3:9

.= dom ((Carrier J2) +* (j,((F . i) .: U))) by FUNCT_7:30 ;

for z being object st z in dom ((Carrier J2) +* (j,((F . i) .: U))) holds

h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z

end;then consider x being object such that

A8: ( x in dom H & x in product ((Carrier J1) +* (i,U)) & y = H . x ) by FUNCT_1:def 6;

reconsider g = x as Element of (product J1) by A8;

y in rng H by A8, FUNCT_1:3;

then reconsider h = y as Element of (product J2) ;

h in the carrier of (product J2) ;

then A9: h in product (Carrier J2) by WAYBEL18:def 3;

then A10: dom h = dom (Carrier J2) by CARD_3:9

.= dom ((Carrier J2) +* (j,((F . i) .: U))) by FUNCT_7:30 ;

for z being object st z in dom ((Carrier J2) +* (j,((F . i) .: U))) holds

h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z

proof

hence
y in product ((Carrier J2) +* (j,((F . i) .: U)))
by A10, CARD_3:9; :: thesis: verum
let z be object ; :: thesis: ( z in dom ((Carrier J2) +* (j,((F . i) .: U))) implies h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z )

assume a11: z in dom ((Carrier J2) +* (j,((F . i) .: U))) ; :: thesis: h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z

then A11: z in dom (Carrier J2) by FUNCT_7:30;

reconsider j0 = z as Element of I2 by a11;

I2 = rng p by A1, FUNCT_2:def 3;

then consider i0 being object such that

A12: ( i0 in I1 & p . i0 = j0 ) by FUNCT_2:11;

reconsider i0 = i0 as Element of I1 by A12;

consider f0 being Function of (J1 . i0),((J2 * p) . i0) such that

A13: ( F . i0 = f0 & f0 is being_homeomorphism ) by A2;

A14: h . j0 = f0 . (g . i0) by A3, A8, A12, A13;

end;assume a11: z in dom ((Carrier J2) +* (j,((F . i) .: U))) ; :: thesis: h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z

then A11: z in dom (Carrier J2) by FUNCT_7:30;

reconsider j0 = z as Element of I2 by a11;

I2 = rng p by A1, FUNCT_2:def 3;

then consider i0 being object such that

A12: ( i0 in I1 & p . i0 = j0 ) by FUNCT_2:11;

reconsider i0 = i0 as Element of I1 by A12;

consider f0 being Function of (J1 . i0),((J2 * p) . i0) such that

A13: ( F . i0 = f0 & f0 is being_homeomorphism ) by A2;

A14: h . j0 = f0 . (g . i0) by A3, A8, A12, A13;

per cases
( j0 = j or j0 <> j )
;

end;

suppose A15:
j0 = j
; :: thesis: h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z

then A16:
((Carrier J2) +* (j,((F . i) .: U))) . z = (F . i) .: U
by A11, FUNCT_7:31;

A17: i0 = i by A1, A12, A15, FUNCT_2:19;

a18: I1 = dom (Carrier J1) by PARTFUN1:def 2;

then i in dom (Carrier J1) ;

then i in dom ((Carrier J1) +* (i,U)) by FUNCT_7:30;

then g . i in ((Carrier J1) +* (i,U)) . i by A8, CARD_3:9;

then g . i in U by a18, FUNCT_7:31;

hence h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z by A14, A16, A17, A13, FUNCT_2:35; :: thesis: verum

end;A17: i0 = i by A1, A12, A15, FUNCT_2:19;

a18: I1 = dom (Carrier J1) by PARTFUN1:def 2;

then i in dom (Carrier J1) ;

then i in dom ((Carrier J1) +* (i,U)) by FUNCT_7:30;

then g . i in ((Carrier J1) +* (i,U)) . i by A8, CARD_3:9;

then g . i in U by a18, FUNCT_7:31;

hence h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z by A14, A16, A17, A13, FUNCT_2:35; :: thesis: verum

then reconsider h = y as Element of product ((Carrier J2) +* (j,((F . i) .: U))) ;

A21: the carrier of (J1 . i) = [#] (J1 . i) by STRUCT_0:def 3

.= (Carrier J1) . i by PENCIL_3:7 ;

i in I1 ;

then A22: i in dom (Carrier J1) by PARTFUN1:def 2;

then A23: product ((Carrier J1) +* (i,U)) c= product (Carrier J1) by A21, Th39;

A24: (Carrier J2) . j = [#] (J2 . j) by PENCIL_3:7

.= the carrier of (J2 . j) by STRUCT_0:def 3 ;

a25: ( j in I2 & (F . i) .: U c= the carrier of (J2 . j) ) by A6, A5, RELAT_1:111;

then A25: ( j in dom (Carrier J2) & (F . i) .: U c= (Carrier J2) . j ) by A24, PARTFUN1:def 2;

then A26: product ((Carrier J2) +* (j,((F . i) .: U))) c= product (Carrier J2) by Th39;

ex x being object st

( x in dom H & x in product ((Carrier J1) +* (i,U)) & H . x = y )

proof

hence
y in H .: (product ((Carrier J1) +* (i,U)))
by FUNCT_1:def 6; :: thesis: verum
defpred S_{1}[ object , object ] means ex f being one-to-one Function st

( F . $1 = f & $2 = (f ") . (h . (p . $1)) );

A28: for i0 being Element of I1 ex y being object st S_{1}[i0,y]

A30: for i being Element of I1 holds S_{1}[i,g . i]
from PBOOLE:sch 6(A28);

take g ; :: thesis: ( g in dom H & g in product ((Carrier J1) +* (i,U)) & H . g = y )

A31: dom g = I1 by PARTFUN1:def 2

.= dom ((Carrier J1) +* (i,U)) by PARTFUN1:def 2 ;

a36: for z being object st z in dom ((Carrier J1) +* (i,U)) holds

g . z in ((Carrier J1) +* (i,U)) . z

then g in product (Carrier J1) by A23;

then A47: g in the carrier of (product J1) by WAYBEL18:def 3;

hence ( g in dom H & g in product ((Carrier J1) +* (i,U)) ) by a36, A31, CARD_3:9, FUNCT_2:def 1; :: thesis: H . g = y

reconsider h0 = H . g as Element of (product J2) by A47, FUNCT_2:5;

h0 in the carrier of (product J2) ;

then h0 in product (Carrier J2) by WAYBEL18:def 3;

then A48: dom h0 = dom (Carrier J2) by CARD_3:9

.= dom h by A20, A26, CARD_3:9 ;

for z being object st z in dom h holds

h . z = h0 . z

end;( F . $1 = f & $2 = (f ") . (h . (p . $1)) );

A28: for i0 being Element of I1 ex y being object st S

proof

consider g being ManySortedSet of I1 such that
let i0 be Element of I1; :: thesis: ex y being object st S_{1}[i0,y]

consider f0 being Function of (J1 . i0),((J2 * p) . i0) such that

A29: ( F . i0 = f0 & f0 is being_homeomorphism ) by A2;

reconsider f0 = f0 as one-to-one Function by A29;

take (f0 ") . (h . (p . i0)) ; :: thesis: S_{1}[i0,(f0 ") . (h . (p . i0))]

take f0 ; :: thesis: ( F . i0 = f0 & (f0 ") . (h . (p . i0)) = (f0 ") . (h . (p . i0)) )

thus ( F . i0 = f0 & (f0 ") . (h . (p . i0)) = (f0 ") . (h . (p . i0)) ) by A29; :: thesis: verum

end;consider f0 being Function of (J1 . i0),((J2 * p) . i0) such that

A29: ( F . i0 = f0 & f0 is being_homeomorphism ) by A2;

reconsider f0 = f0 as one-to-one Function by A29;

take (f0 ") . (h . (p . i0)) ; :: thesis: S

take f0 ; :: thesis: ( F . i0 = f0 & (f0 ") . (h . (p . i0)) = (f0 ") . (h . (p . i0)) )

thus ( F . i0 = f0 & (f0 ") . (h . (p . i0)) = (f0 ") . (h . (p . i0)) ) by A29; :: thesis: verum

A30: for i being Element of I1 holds S

take g ; :: thesis: ( g in dom H & g in product ((Carrier J1) +* (i,U)) & H . g = y )

A31: dom g = I1 by PARTFUN1:def 2

.= dom ((Carrier J1) +* (i,U)) by PARTFUN1:def 2 ;

a36: for z being object st z in dom ((Carrier J1) +* (i,U)) holds

g . z in ((Carrier J1) +* (i,U)) . z

proof

then
g in product ((Carrier J1) +* (i,U))
by A31, CARD_3:9;
let z be object ; :: thesis: ( z in dom ((Carrier J1) +* (i,U)) implies g . z in ((Carrier J1) +* (i,U)) . z )

assume z in dom ((Carrier J1) +* (i,U)) ; :: thesis: g . z in ((Carrier J1) +* (i,U)) . z

then reconsider i0 = z as Element of I1 ;

consider f0 being one-to-one Function such that

A32: ( F . i0 = f0 & g . i0 = (f0 ") . (h . (p . i0)) ) by A30;

p . i0 in I2 ;

then p . i0 in dom (Carrier J2) by PARTFUN1:def 2;

then h . (p . i0) in (Carrier J2) . (p . i0) by A20, A26, CARD_3:9;

then h . (p . i0) in [#] (J2 . (p . i0)) by PENCIL_3:7;

then A33: h . (p . i0) in [#] ((J2 * p) . i0) by FUNCT_2:15;

end;assume z in dom ((Carrier J1) +* (i,U)) ; :: thesis: g . z in ((Carrier J1) +* (i,U)) . z

then reconsider i0 = z as Element of I1 ;

consider f0 being one-to-one Function such that

A32: ( F . i0 = f0 & g . i0 = (f0 ") . (h . (p . i0)) ) by A30;

p . i0 in I2 ;

then p . i0 in dom (Carrier J2) by PARTFUN1:def 2;

then h . (p . i0) in (Carrier J2) . (p . i0) by A20, A26, CARD_3:9;

then h . (p . i0) in [#] (J2 . (p . i0)) by PENCIL_3:7;

then A33: h . (p . i0) in [#] ((J2 * p) . i0) by FUNCT_2:15;

per cases
( i = i0 or i <> i0 )
;

end;

suppose A35:
i = i0
; :: thesis: g . z in ((Carrier J1) +* (i,U)) . z

then A36:
((Carrier J1) +* (i,U)) . z = U
by A22, FUNCT_7:31;

j in dom ((Carrier J2) +* (j,((F . i) .: U))) by a25, PARTFUN1:def 2;

then h . j in ((Carrier J2) +* (j,((F . i) .: U))) . j by A20, CARD_3:9;

then A37: h . j in (F . i) .: U by A25, FUNCT_7:31;

A38: f " = f0 " by A5, A32, A35, TOPS_2:def 4;

[#] ((J2 * p) . i0) = rng f by A5, A35, TOPS_2:def 5

.= dom (f0 ") by A5, A32, A35, FUNCT_1:33 ;

then g . i0 in rng (f0 ") by A32, A33, FUNCT_1:3;

then A39: g . i0 in dom f by A5, A32, A35, FUNCT_1:33;

h . j in (Carrier J2) . j by A20, A26, A25, CARD_3:9;

then h . j in [#] (J2 . j) by PENCIL_3:7;

then a40: h . j in [#] ((J2 * p) . i) by A4, FUNCT_1:13;

a41: dom f = the carrier of (J1 . i) by FUNCT_2:def 1;

reconsider f1 = f as one-to-one Function by A5;

A43: h . j in rng f1 by a40, A5, TOPS_2:def 5;

f . ((f ") . (h . j)) = f1 . ((f1 ") . (h . j)) by A5, TOPS_2:def 4

.= h . j by A43, FUNCT_1:35 ;

then g . i0 in f0 " (f0 .: U) by A5, A32, A35, A38, A39, A37, FUNCT_1:def 7;

hence g . z in ((Carrier J1) +* (i,U)) . z by A36, a41, A5, A32, A35, FUNCT_1:94; :: thesis: verum

end;j in dom ((Carrier J2) +* (j,((F . i) .: U))) by a25, PARTFUN1:def 2;

then h . j in ((Carrier J2) +* (j,((F . i) .: U))) . j by A20, CARD_3:9;

then A37: h . j in (F . i) .: U by A25, FUNCT_7:31;

A38: f " = f0 " by A5, A32, A35, TOPS_2:def 4;

[#] ((J2 * p) . i0) = rng f by A5, A35, TOPS_2:def 5

.= dom (f0 ") by A5, A32, A35, FUNCT_1:33 ;

then g . i0 in rng (f0 ") by A32, A33, FUNCT_1:3;

then A39: g . i0 in dom f by A5, A32, A35, FUNCT_1:33;

h . j in (Carrier J2) . j by A20, A26, A25, CARD_3:9;

then h . j in [#] (J2 . j) by PENCIL_3:7;

then a40: h . j in [#] ((J2 * p) . i) by A4, FUNCT_1:13;

a41: dom f = the carrier of (J1 . i) by FUNCT_2:def 1;

reconsider f1 = f as one-to-one Function by A5;

A43: h . j in rng f1 by a40, A5, TOPS_2:def 5;

f . ((f ") . (h . j)) = f1 . ((f1 ") . (h . j)) by A5, TOPS_2:def 4

.= h . j by A43, FUNCT_1:35 ;

then g . i0 in f0 " (f0 .: U) by A5, A32, A35, A38, A39, A37, FUNCT_1:def 7;

hence g . z in ((Carrier J1) +* (i,U)) . z by A36, a41, A5, A32, A35, FUNCT_1:94; :: thesis: verum

suppose
i <> i0
; :: thesis: g . z in ((Carrier J1) +* (i,U)) . z

then A44:
((Carrier J1) +* (i,U)) . z = (Carrier J1) . z
by FUNCT_7:32;

consider f9 being Function of (J1 . i0),((J2 * p) . i0) such that

A45: ( F . i0 = f9 & f9 is being_homeomorphism ) by A2;

dom (f0 ") = rng f0 by FUNCT_1:33

.= [#] ((J2 * p) . i0) by A32, A45, TOPS_2:def 5

.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;

then (f0 ") . (h . (p . i0)) in rng (f0 ") by A33, FUNCT_1:3;

then g . i0 in dom f0 by A32, FUNCT_1:33;

then g . i0 in [#] (J1 . i0) by A32, A45, TOPS_2:def 5;

hence g . z in ((Carrier J1) +* (i,U)) . z by A44, PENCIL_3:7; :: thesis: verum

end;consider f9 being Function of (J1 . i0),((J2 * p) . i0) such that

A45: ( F . i0 = f9 & f9 is being_homeomorphism ) by A2;

dom (f0 ") = rng f0 by FUNCT_1:33

.= [#] ((J2 * p) . i0) by A32, A45, TOPS_2:def 5

.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;

then (f0 ") . (h . (p . i0)) in rng (f0 ") by A33, FUNCT_1:3;

then g . i0 in dom f0 by A32, FUNCT_1:33;

then g . i0 in [#] (J1 . i0) by A32, A45, TOPS_2:def 5;

hence g . z in ((Carrier J1) +* (i,U)) . z by A44, PENCIL_3:7; :: thesis: verum

then g in product (Carrier J1) by A23;

then A47: g in the carrier of (product J1) by WAYBEL18:def 3;

hence ( g in dom H & g in product ((Carrier J1) +* (i,U)) ) by a36, A31, CARD_3:9, FUNCT_2:def 1; :: thesis: H . g = y

reconsider h0 = H . g as Element of (product J2) by A47, FUNCT_2:5;

h0 in the carrier of (product J2) ;

then h0 in product (Carrier J2) by WAYBEL18:def 3;

then A48: dom h0 = dom (Carrier J2) by CARD_3:9

.= dom h by A20, A26, CARD_3:9 ;

for z being object st z in dom h holds

h . z = h0 . z

proof

hence
H . g = y
by A48, FUNCT_1:2; :: thesis: verum
let z be object ; :: thesis: ( z in dom h implies h . z = h0 . z )

assume z in dom h ; :: thesis: h . z = h0 . z

then z in dom (Carrier J2) by A20, A26, CARD_3:9;

then reconsider j0 = z as Element of I2 ;

reconsider p9 = p as one-to-one Function by A1;

j0 in I2 ;

then A49: j0 in rng p9 by A1, FUNCT_2:def 3;

then j0 in dom (p9 ") by FUNCT_1:33;

then (p9 ") . j0 in rng (p9 ") by FUNCT_1:3;

then A50: (p9 ") . j0 in dom p9 by FUNCT_1:33;

then reconsider i0 = (p9 ") . j0 as Element of I1 by FUNCT_2:def 1;

consider f9 being one-to-one Function such that

A51: ( F . i0 = f9 & g . i0 = (f9 ") . (h . (p . i0)) ) by A30;

consider f0 being Function of (J1 . i0),((J2 * p) . i0) such that

A52: ( F . i0 = f0 & f0 is being_homeomorphism ) by A2;

A53: rng f9 = [#] ((J2 * p) . i0) by A51, A52, TOPS_2:def 5

.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;

A54: p . i0 = j0 by A49, FUNCT_1:35;

A55: (Carrier J2) . (p . i0) = [#] (J2 . (p . i0)) by PENCIL_3:7

.= [#] ((J2 * p) . i0) by A50, FUNCT_1:13

.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;

p . i0 in I2 ;

then p . i0 in dom (Carrier J2) by PARTFUN1:def 2;

then A56: h . (p . i0) in (Carrier J2) . (p . i0) by A20, A26, CARD_3:9;

h . j0 = f9 . ((f9 ") . (h . (p . i0))) by A53, A54, A55, A56, FUNCT_1:35

.= h0 . j0 by A3, A47, A51, A54 ;

hence h . z = h0 . z ; :: thesis: verum

end;assume z in dom h ; :: thesis: h . z = h0 . z

then z in dom (Carrier J2) by A20, A26, CARD_3:9;

then reconsider j0 = z as Element of I2 ;

reconsider p9 = p as one-to-one Function by A1;

j0 in I2 ;

then A49: j0 in rng p9 by A1, FUNCT_2:def 3;

then j0 in dom (p9 ") by FUNCT_1:33;

then (p9 ") . j0 in rng (p9 ") by FUNCT_1:3;

then A50: (p9 ") . j0 in dom p9 by FUNCT_1:33;

then reconsider i0 = (p9 ") . j0 as Element of I1 by FUNCT_2:def 1;

consider f9 being one-to-one Function such that

A51: ( F . i0 = f9 & g . i0 = (f9 ") . (h . (p . i0)) ) by A30;

consider f0 being Function of (J1 . i0),((J2 * p) . i0) such that

A52: ( F . i0 = f0 & f0 is being_homeomorphism ) by A2;

A53: rng f9 = [#] ((J2 * p) . i0) by A51, A52, TOPS_2:def 5

.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;

A54: p . i0 = j0 by A49, FUNCT_1:35;

A55: (Carrier J2) . (p . i0) = [#] (J2 . (p . i0)) by PENCIL_3:7

.= [#] ((J2 * p) . i0) by A50, FUNCT_1:13

.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;

p . i0 in I2 ;

then p . i0 in dom (Carrier J2) by PARTFUN1:def 2;

then A56: h . (p . i0) in (Carrier J2) . (p . i0) by A20, A26, CARD_3:9;

h . j0 = f9 . ((f9 ") . (h . (p . i0))) by A53, A54, A55, A56, FUNCT_1:35

.= h0 . j0 by A3, A47, A51, A54 ;

hence h . z = h0 . z ; :: thesis: verum