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 ( Seg j = {} implies Seg i = {} ) ;
then A1: dom f = Seg i by FUNCT_2:def 1;
assume j <= len p ; :: thesis: p * f is FinSequence
then ( rng f c= Seg j & Seg j c= Seg (len p) ) by FINSEQ_1:5, RELAT_1:def 19;
then rng f c= Seg (len p) ;
then rng f c= dom p by FINSEQ_1:def 3;
then dom (p * f) = dom f by RELAT_1:27;
hence p * f is FinSequence by A1, FINSEQ_1:def 2; :: thesis: verum