let f be Function; :: thesis: for p being FinSequence holds
( firstdom (<*f*> ^ p) = dom f & lastrng (p ^ <*f*>) = rng f )
let p be FinSequence; :: thesis: ( firstdom (<*f*> ^ p) = dom f & lastrng (p ^ <*f*>) = rng f )
thus firstdom (<*f*> ^ p) = proj1 ((<*f*> ^ p) . 1) by Def6
.= dom f by FINSEQ_1:58 ; :: thesis: lastrng (p ^ <*f*>) = rng f
len <*f*> = 1 by FINSEQ_1:57;
then len (p ^ <*f*>) = (len p) + 1 by FINSEQ_1:35;
hence lastrng (p ^ <*f*>) = proj2 ((p ^ <*f*>) . ((len p) + 1)) by Def7
.= rng f by FINSEQ_1:59 ;
:: thesis: verum