let I be set ; :: thesis: for f being ManySortedSet of
for p being FinSequence of I holds
( dom (f * p) = dom p & len (f * p) = len p )
let f be ManySortedSet of ; :: 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 )
rng p c= I ;
then A1: rng p c= dom f by PARTFUN1:def 4;
reconsider q = f * p as FinSequence ;
len q = len p by A1, FINSEQ_2:33;
hence ( dom (f * p) = dom p & len (f * p) = len p ) by FINSEQ_3:31; :: thesis: verum