per cases ( m = 0 or m > 0 ) ;

suppose m = 0 ; :: thesis: (idseq (m + n)) . m = m

hence (idseq (m + n)) . m = m ; :: thesis: verum

end;

suppose m > 0 ; :: thesis: (idseq (m + n)) . m = m

then ( m + n >= m + 0 & m >= 1 ) by NAT_1:14, XREAL_1:6;
then m in Seg (m + n) ;
hence (idseq (m + n)) . m = m by FINSEQ_2:49; :: thesis: verum

end;

end;