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 by FUNCOP_1:19;
hence (1_ n,L) . (EmptyBag n) = 1. L by FUNCT_7:33; :: 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:34
.= 0. L by A1, FUNCOP_1:13 ;
:: thesis: verum