let I be set ; :: thesis: for f being ManySortedSet of I
for p being FinSequence of I holds
( dom (f * p) = dom p & len (f * p) = len p )
let f be ManySortedSet of I; :: thesis: for p being FinSequence of I holds
( dom (f * p) = dom p & len (f * p) = len p )
let p be FinSequence of I; :: thesis: ( dom (f * p) = dom p & len (f * p) = len p )
reconsider q = f * p as FinSequence ;
rng p c= I ;
then rng p c= dom f by PARTFUN1:def 2;
then len q = len p by FINSEQ_2:29;
hence ( dom (f * p) = dom p & len (f * p) = len p ) by FINSEQ_3:29; :: thesis: verum