let I be non empty set ; for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being I -valued one-to-one Function st f " is non-empty & dom f c= bool (product (Carrier J)) holds
product_basis_selector (J,f) is non-empty
let J be non-Empty TopStruct-yielding ManySortedSet of I; for f being I -valued one-to-one Function st f " is non-empty & dom f c= bool (product (Carrier J)) holds
product_basis_selector (J,f) is non-empty
let f be I -valued one-to-one Function; ( f " is non-empty & dom f c= bool (product (Carrier J)) implies product_basis_selector (J,f) is non-empty )
assume A1:
( f " is non-empty & dom f c= bool (product (Carrier J)) )
; product_basis_selector (J,f) is non-empty
assume
not product_basis_selector (J,f) is non-empty
; contradiction
then consider x being object such that
A2:
x in dom (product_basis_selector (J,f))
and
A3:
(product_basis_selector (J,f)) . x is empty
by FUNCT_1:def 9;
A4:
x in rng f
by A2;
then reconsider i = x as Element of I ;
(proj (J,i)) .: ((f ") . i) is empty
by A3, A2, Th54;
then
dom (proj (J,i)) misses (f ") . i
by RELAT_1:118;
then
dom (proj ((Carrier J),i)) misses (f ") . i
by WAYBEL18:def 4;
then A5:
product (Carrier J) misses (f ") . i
by CARD_3:def 16;
A6:
rng (f ") c= bool (product (Carrier J))
by A1, FUNCT_1:33;
i in dom (f ")
by A4, FUNCT_1:33;
then
(f ") . i in rng (f ")
by FUNCT_1:3;
hence
contradiction
by A1, A5, A6, XBOOLE_1:67; verum