reconsider g = g as empty-yielding n + 0 -element complex-valued FinSequence ;
f + g = f ;
hence f + g = f ; :: thesis: verum