let i, j be Nat; :: thesis: for p being FinSequence
for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence
let p be FinSequence; :: thesis: for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence
let f be Function of (Seg i),(Seg j); :: thesis: ( ( j = 0 implies i = 0 ) & j <= len p implies p * f is FinSequence )
assume ( j = 0 implies i = 0 ) ; :: thesis: ( not j <= len p or p * f is FinSequence )
then A1: ( Seg j = {} implies Seg i = {} ) ;
assume j <= len p ; :: thesis: p * f is FinSequence
then ( rng f c= Seg j & Seg j c= Seg (len p) ) by FINSEQ_1:7, RELAT_1:def 19;
then rng f c= Seg (len p) by XBOOLE_1:1;
then rng f c= dom p by FINSEQ_1:def 3;
then ( dom (p * f) = dom f & dom f = Seg i ) by A1, FUNCT_2:def 1, RELAT_1:46;
hence p * f is FinSequence by FINSEQ_1:def 2; :: thesis: verum