let n be set ; :: thesis: for L being non empty right_unital multLoopStr_0 holds
( (1_ (n,L)) . (EmptyBag n) = 1. L & ( for b being bag of n st b <> EmptyBag n holds
(1_ (n,L)) . b = 0. L ) )
let L be non empty right_unital multLoopStr_0 ; :: thesis: ( (1_ (n,L)) . (EmptyBag n) = 1. L & ( for b being bag of n st b <> EmptyBag n holds
(1_ (n,L)) . b = 0. L ) )
set Z = 0_ (n,L);
dom (0_ (n,L)) = Bags n ;
hence (1_ (n,L)) . (EmptyBag n) = 1. L by FUNCT_7:31; :: thesis: for b being bag of n st b <> EmptyBag n holds
(1_ (n,L)) . b = 0. L
let b be bag of n; :: thesis: ( b <> EmptyBag n implies (1_ (n,L)) . b = 0. L )
A1: b in Bags n by PRE_POLY:def 12;
assume b <> EmptyBag n ; :: thesis: (1_ (n,L)) . b = 0. L
hence (1_ (n,L)) . b = (0_ (n,L)) . b by FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
:: thesis: verum