let X be set ; :: thesis: for b being bag of X holds support ((2 (#) b) +* (0,(b . 0))) = support b
let b be bag of X; :: thesis: support ((2 (#) b) +* (0,(b . 0))) = support b
A1: ( dom b = X & X = dom (2 (#) b) & X = dom ((2 (#) b) +* (0,(b . 0))) ) by PARTFUN1:def 2;
A2: support ((2 (#) b) +* (0,(b . 0))) c= support b
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support ((2 (#) b) +* (0,(b . 0))) or x in support b )
assume A3: x in support ((2 (#) b) +* (0,(b . 0))) ; :: thesis: x in support b
then A4: ((2 (#) b) +* (0,(b . 0))) . x <> 0 by PRE_POLY:def 7;
per cases ( x = 0 or x <> 0 ) ;
suppose x <> 0 ; :: thesis: x in support b
then ((2 (#) b) +* (0,(b . 0))) . x = (2 (#) b) . x by FUNCT_7:32
.= 2 * (b . x) by VALUED_1:6 ;
then b . x <> 0 by A3, PRE_POLY:def 7;
hence x in support b by PRE_POLY:def 7; :: thesis: verum
end;
end;
end;
support b c= support ((2 (#) b) +* (0,(b . 0)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support b or x in support ((2 (#) b) +* (0,(b . 0))) )
assume A5: x in support b ; :: thesis: x in support ((2 (#) b) +* (0,(b . 0)))
then A6: b . x <> 0 by PRE_POLY:def 7;
per cases ( x = 0 or x <> 0 ) ;
suppose x = 0 ; :: thesis: x in support ((2 (#) b) +* (0,(b . 0)))
then ((2 (#) b) +* (0,(b . 0))) . x = b . x by A5, A1, FUNCT_7:31;
hence x in support ((2 (#) b) +* (0,(b . 0))) by A6, PRE_POLY:def 7; :: thesis: verum
end;
suppose x <> 0 ; :: thesis: x in support ((2 (#) b) +* (0,(b . 0)))
then ((2 (#) b) +* (0,(b . 0))) . x = (2 (#) b) . x by FUNCT_7:32
.= 2 * (b . x) by VALUED_1:6 ;
then ((2 (#) b) +* (0,(b . 0))) . x <> 0 by A5, PRE_POLY:def 7;
hence x in support ((2 (#) b) +* (0,(b . 0))) by PRE_POLY:def 7; :: thesis: verum
end;
end;
end;
hence support ((2 (#) b) +* (0,(b . 0))) = support b by A2, XBOOLE_0:def 10; :: thesis: verum