Suggestion: Revising FINSEQ_1:20

FINSEQ_1:20 is a nice little minitheorem on composing finite sequences with other functions:

for f being Function
for p being FinSequence st rng p c= dom f holds
f * p is FinSequence
proof
 let f be Function;
 let p be FinSequence;
 assume rng p c= dom f ;
 then dom (f * p) = dom p by RELAT_1:46
 .= Seg (len p) by Def3 ;
 hence f * p is FinSequence by Def2;
 end;

This proof shows not only that f*p is of type FinSequence?, but it also tells us that len (f*p) = len p. It would be nice if the theorem gave us that in the conclusion; that way, one wouldn't have to carry out this little proof to get the length of f*p. The new proof would be:

for f being Function
for p being FinSequence st rng p c= dom f holds
f * p is FinSequence & dom (f * p) = Seg (len p)
proof
 let f be Function;
 let p be FinSequence;
 assume rng p c= dom f ;
 then dom (f * p) = dom p by RELAT_1:46
 .= Seg (len p) by Def3 ;
 hence f * p is FinSequence & dom (f *p) = Seg (len p) by Def2;
 end;

Article name:	FINSEQ_1
MML version:	4.81.962

|

Follow up

Hmm, it seems that I spoke too quickly: FINSEQ_2:33 is relevant here:

for p, q being FinSequence
for f being Function st rng p c= dom f & q = f * p holds
len q = len p

Putting together FINSEQ_1:20 and FINSEQ_2:33 gives the desired result.