let x1, x2 be complex-valued FinSequence; :: thesis: ( len x1 <= len x2 implies len (x1 + x2) = len x1 )
assume len x1 <= len x2 ; :: thesis: len (x1 + x2) = len x1
then A2: dom x1 c= dom x2 by FINSEQ_3:30;
dom (x1 + x2) = (dom x1) /\ (dom x2) by VALUED_1:def 1;
hence len (x1 + x2) = len x1 by A2, XBOOLE_1:28, FINSEQ_3:29; :: thesis: verum