let L be non empty ZeroStr ; :: thesis: for x being Element of L
for f being the carrier of L -valued Function
for a being object holds Support (f +* (a,x)) c= (Support f) \/ {a}
let x be Element of L; :: thesis: for f being the carrier of L -valued Function
for a being object holds Support (f +* (a,x)) c= (Support f) \/ {a}
let f be the carrier of L -valued Function; :: thesis: for a being object holds Support (f +* (a,x)) c= (Support f) \/ {a}
let a, z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Support (f +* (a,x)) or z in (Support f) \/ {a} )
set g = f +* (a,x);
assume A1: z in Support (f +* (a,x)) ; :: thesis: z in (Support f) \/ {a}
( a = z or z in Support f )
proof
assume a <> z ; :: thesis: z in Support f
then A2: (f +* (a,x)) . z = f . z by FUNCT_7:32;
dom (f +* (a,x)) = dom f by FUNCT_7:30;
then ( z in dom f & (f +* (a,x)) . z <> 0. L ) by A1, POLYNOM1:def 3;
hence z in Support f by A2, POLYNOM1:def 3; :: thesis: verum
end;
hence z in (Support f) \/ {a} by ZFMISC_1:136; :: thesis: verum