let I be non empty set ; for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
( f is onto & f is open )
let J be non-Empty TopSpace-yielding ManySortedSet of I; for i, j being Element of I
for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
( f is onto & f is open )
let i, j be Element of I; for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
( f is onto & f is open )
let f be Function of (product J),[:(J . i),(J . j):]; ( i <> j & f = <:(proj (J,i)),(proj (J,j)):> implies ( f is onto & f is open ) )
assume A1:
( i <> j & f = <:(proj (J,i)),(proj (J,j)):> )
; ( f is onto & f is open )
a2:
for k being Element of I holds (Carrier J) . k c= (Carrier J) . k
;
A3:
for k being Element of I holds (proj (J,k)) .: ([#] (product (Carrier J))) = the carrier of (J . k)
rng f =
<:(proj (J,i)),(proj (J,j)):> .: (dom f)
by A1, RELAT_1:113
.=
<:(proj (J,i)),(proj (J,j)):> .: the carrier of (product J)
by FUNCT_2:def 1
.=
<:(proj (J,i)),(proj (J,j)):> .: (product (Carrier J))
by WAYBEL18:def 3
.=
<:(proj (J,i)),(proj (J,j)):> .: ([#] (product (Carrier J)))
by SUBSET_1:def 3
.=
[:((proj (J,i)) .: ([#] (product (Carrier J)))),((proj (J,j)) .: ([#] (product (Carrier J)))):]
by A1, SUBSET_1:def 3, a2, Th72
.=
[: the carrier of (J . i),((proj (J,j)) .: ([#] (product (Carrier J)))):]
by A3
.=
[: the carrier of (J . i), the carrier of (J . j):]
by A3
.=
the carrier of [:(J . i),(J . j):]
by BORSUK_1:def 2
;
hence
f is onto
by FUNCT_2:def 3; f is open
ex B being Basis of (product J) st
for P being Subset of (product J) st P in B holds
f .: P is open
hence
f is open
by Th45; verum