let I be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: product_basis_selector (J,f) is non-empty

assume not product_basis_selector (J,f) is non-empty ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: product_basis_selector (J,f) is non-empty

assume not product_basis_selector (J,f) is non-empty ; :: thesis: 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; :: thesis: verum