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

proof

let o be object ; :: thesis: ( o in dom ((0_. R) +* (1,(1. R))) implies (((0_ (1,R)) +* ((1 --> 1),(1. R))) * NBag1) . o = ((0_. R) +* (1,(1. R))) . o )
assume A2: o in dom ((0_. R) +* (1,(1. R))) ; :: thesis: (((0_ (1,R)) +* ((1 --> 1),(1. R))) * NBag1) . o = ((0_. R) +* (1,(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: 1 --> 1 in dom (0_ (1,R)) by PRE_POLY:def 12;
A5: 1 in dom (0_. R) ;

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

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

then NBag1 . o = 1 --> 1 by Def1;
then (((0_ (1,R)) +* ((1 --> 1),(1. R))) * NBag1) . o = ((0_ (1,R)) +* ((1 --> 1),(1. R))) . (1 --> 1) by A2, FUNCT_2:15
.= 1. R by A4, FUNCT_7:31
.= ((0_. R) +* (1,(1. R))) . 1 by A5, FUNCT_7:31 ;
hence (((0_ (1,R)) +* ((1 --> 1),(1. R))) * NBag1) . o = ((0_. R) +* (1,(1. R))) . o by A6; :: thesis: verum

end;

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

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

end;

end;

end;

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