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

for i being Element of I st i in rng f holds

(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for f being I -valued one-to-one Function

for i being Element of I st i in rng f holds

(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

let f be I -valued one-to-one Function; :: thesis: for i being Element of I st i in rng f holds

(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

let i be Element of I; :: thesis: ( i in rng f implies (product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i) )

assume A1: i in rng f ; :: thesis: (product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

then A2: i in dom (f ") by FUNCT_1:33;

thus (product_basis_selector (J,f)) . i = ((ProjMap J) .:.: (I -indexing (f "))) . i by A1, FUNCT_1:49

.= ((ProjMap J) . i) .: ((I -indexing (f ")) . i) by PBOOLE:def 20

.= (proj (J,i)) .: ((I -indexing (f ")) . i) by Th53

.= (proj (J,i)) .: ((f ") . i) by A2, ALGSPEC1:9 ; :: thesis: verum

for f being I -valued one-to-one Function

for i being Element of I st i in rng f holds

(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for f being I -valued one-to-one Function

for i being Element of I st i in rng f holds

(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

let f be I -valued one-to-one Function; :: thesis: for i being Element of I st i in rng f holds

(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

let i be Element of I; :: thesis: ( i in rng f implies (product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i) )

assume A1: i in rng f ; :: thesis: (product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)

then A2: i in dom (f ") by FUNCT_1:33;

thus (product_basis_selector (J,f)) . i = ((ProjMap J) .:.: (I -indexing (f "))) . i by A1, FUNCT_1:49

.= ((ProjMap J) . i) .: ((I -indexing (f ")) . i) by PBOOLE:def 20

.= (proj (J,i)) .: ((I -indexing (f ")) . i) by Th53

.= (proj (J,i)) .: ((f ") . i) by A2, ALGSPEC1:9 ; :: thesis: verum