let g be sequence of L; :: thesis: ( g = f +* (a,x) implies g is finite-Support )
assume A1: g = f +* (a,x) ; :: thesis: g is finite-Support
A2: f is finite-Support ;
Support g c= (Support f) \/ {a} by A1, Th21;
hence g is finite-Support by A2; :: thesis: verum