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

proof

let o be object ; :: thesis: ( o in dom (NBag1 * BagN1) implies (NBag1 * BagN1) . o = (id (Bags 1)) . o )
assume o in dom (NBag1 * BagN1) ; :: thesis: (NBag1 * BagN1) . o = (id (Bags 1)) . o
then reconsider b = o as Element of Bags 1 ;
A1: BagN1 . o = b . 0 by Def2;
(NBag1 * BagN1) . o = NBag1 . (b . 0) by A1, FUNCT_2:15
.= 1 --> (b . 0) by Def1
.= (id (Bags 1)) . o by Th5 ;
hence (NBag1 * BagN1) . o = (id (Bags 1)) . o ; :: thesis: verum

end;

hence NBag1 * BagN1 = id (Bags 1) by FUNCT_2:def 1; :: thesis: verum