let R be non degenerated comRing; :: thesis: ((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1 = (0_. R) +* (0,(1. R))
A1: dom ((0_. R) +* (0,(1. R))) = NAT by FUNCT_2:def 1
.= dom (((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) by FUNCT_2:def 1 ;
for o being object st o in dom ((0_. R) +* (0,(1. R))) holds
(((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) . o = ((0_. R) +* (0,(1. R))) . o

proof

let o be object ; :: thesis: ( o in dom ((0_. R) +* (0,(1. R))) implies (((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) . o = ((0_. R) +* (0,(1. R))) . o )
assume A2: o in dom ((0_. R) +* (0,(1. R))) ; :: thesis: (((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) . o = ((0_. R) +* (0,(1. R))) . o
then reconsider m = o as Element of NAT ;
A3: NBag1 . o = 1 --> m by Def1;
reconsider b = NBag1 . o as Element of Bags 1 by A3, PRE_POLY:def 12;
A4: EmptyBag 1 in dom (0_ (1,R)) ;
A5: 0 in dom (0_. R) ;

per cases ( m = 0 or m <> 0 ) ;

suppose A6: m = 0 ; :: thesis: (((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) . o = ((0_. R) +* (0,(1. R))) . o

then NBag1 . o = EmptyBag 1 by A3, PBOOLE:def 3;
then (((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) . o = ((0_ (1,R)) +* ((EmptyBag 1),(1. R))) . (EmptyBag 1) by A2, FUNCT_2:15
.= 1. R by A4, FUNCT_7:31
.= ((0_. R) +* (0,(1. R))) . 0 by A5, FUNCT_7:31 ;
hence (((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) . o = ((0_. R) +* (0,(1. R))) . o by A6; :: thesis: verum

end;

suppose A7: m <> 0 ; :: thesis: (((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) . o = ((0_. R) +* (0,(1. R))) . o

A8: 1 --> m in Bags 1 by PRE_POLY:def 12;
(((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) . o = ((0_ (1,R)) +* ((EmptyBag 1),(1. R))) . (1 --> m) by A3, FUNCT_2:15
.= ((Bags 1) --> (0. R)) . (1 --> m) by A7, FUNCT_7:32
.= (0_. R) . o by A8, FUNCOP_1:7
.= ((0_. R) +* (0,(1. R))) . o by A7, FUNCT_7:32 ;
hence (((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1) . o = ((0_. R) +* (0,(1. R))) . o ; :: thesis: verum

end;

end;

end;

hence ((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1 = (0_. R) +* (0,(1. R)) by A1; :: thesis: verum