let p, q be FinSequence; :: thesis: for f being Function st rng p c= dom f & q = f * p holds
len q = len p
let f be Function; :: thesis: ( rng p c= dom f & q = f * p implies len q = len p )
assume rng p c= dom f ; :: thesis: ( not q = f * p or len q = len p )
then dom (f * p) = dom p by RELAT_1:27;
then dom (f * p) = Seg (len p) by FINSEQ_1:def 3;
hence ( not q = f * p or len q = len p ) by FINSEQ_1:def 3; :: thesis: verum