let i be natural Number ; :: thesis: for p, q being FinSequence
for f being Function of (Seg i),(Seg i) st rng f = Seg i & i <= len p & q = p * f holds
len q = i
let p, q be FinSequence; :: thesis: for f being Function of (Seg i),(Seg i) st rng f = Seg i & i <= len p & q = p * f holds
len q = i
let f be Function of (Seg i),(Seg i); :: thesis: ( rng f = Seg i & i <= len p & q = p * f implies len q = i )
assume ( rng f = Seg i & i <= len p ) ; :: thesis: ( not q = p * f or len q = i )
then rng f c= Seg (len p) by FINSEQ_1:5;
then rng f c= dom p by FINSEQ_1:def 3;
then A1: dom (p * f) = dom f by RELAT_1:27;
( i is Element of NAT & dom f = Seg i ) by FUNCT_2:52, ORDINAL1:def 12;
hence ( not q = p * f or len q = i ) by A1, FINSEQ_1:def 3; :: thesis: verum