for o being object st o in dom (BagN1 * NBag1) holds
(BagN1 * NBag1) . o = (id NAT) . o

proof

let o be object ; :: thesis: ( o in dom (BagN1 * NBag1) implies (BagN1 * NBag1) . o = (id NAT) . o )
assume A1: o in dom (BagN1 * NBag1) ; :: thesis: (BagN1 * NBag1) . o = (id NAT) . 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;
A3: 1 --> m = b by Def1;
0 in 1 by CARD_1:49, TARSKI:def 1;
then A4: m = b . 0 by A3, FUNCOP_1:7;
(BagN1 * NBag1) . o = BagN1 . b by A1, FUNCT_2:15
.= o by A4, Def2
.= (id NAT) . o by A1, FUNCT_1:18 ;
hence (BagN1 * NBag1) . o = (id NAT) . o ; :: thesis: verum

end;

hence BagN1 * NBag1 = id NAT by FUNCT_2:def 1; :: thesis: verum