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