let R be non degenerated comRing; :: thesis: (0_ (1,R)) * NBag1 = 0_. R
for o being object st o in dom ((0_ (1,R)) * NBag1) holds
((0_ (1,R)) * NBag1) . o = (0_. R) . o

proof

let o be object ; :: thesis: ( o in dom ((0_ (1,R)) * NBag1) implies ((0_ (1,R)) * NBag1) . o = (0_. R) . o )
assume A1: o in dom ((0_ (1,R)) * NBag1) ; :: thesis: ((0_ (1,R)) * NBag1) . o = (0_. R) . o
then reconsider m = o as Element of NAT ;
A2: NBag1 . o = 1 --> m by Def1;
reconsider b = NBag1 . o as Element of Bags 1 by A2, PRE_POLY:def 12;
((0_ (1,R)) * NBag1) . o = (0_ (1,R)) . b by A1, FUNCT_2:15
.= (0_. R) . m
.= (0_. R) . o ;
hence ((0_ (1,R)) * NBag1) . o = (0_. R) . o ; :: thesis: verum

end;

hence (0_ (1,R)) * NBag1 = 0_. R by FUNCT_2:def 1; :: thesis: verum