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