:: deftheorem defines <= INTEGRA1:def 18 :
for D1, D2 being FinSequence holds
( D1 <= D2 iff ( len D1 <= len D2 & rng D1 c= rng D2 ) );