let a be Nat; :: thesis: for X being set
for b being real-valued ManySortedSet of X st a <> 0 holds
support b = support (a * b)
let X be set ; :: thesis: for b being real-valued ManySortedSet of X st a <> 0 holds
support b = support (a * b)
let b be real-valued ManySortedSet of X; :: thesis: ( a <> 0 implies support b = support (a * b) )
assume A1: a <> 0 ; :: thesis: support b = support (a * b)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: support (a * b) c= support b

let x be object ; :: thesis: ( x in support b implies x in support (a * b) )
assume x in support b ; :: thesis: x in support (a * b)
then b . x <> 0 by PRE_POLY:def 7;
then a * (b . x) <> 0 by A1;
then (a * b) . x <> 0 by Def2;
hence x in support (a * b) by PRE_POLY:def 7; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (a * b) or x in support b )
assume x in support (a * b) ; :: thesis: x in support b
then (a * b) . x <> 0 by PRE_POLY:def 7;
then a * (b . x) <> 0 by Def2;
then b . x <> 0 ;
hence x in support b by PRE_POLY:def 7; :: thesis: verum