let n be set ; :: thesis: for L being non empty multLoopStr_0
for a being Element of L holds
( (a | n,L) . (EmptyBag n) = a & ( for b being bag of n st b <> EmptyBag n holds
(a | n,L) . b = 0. L ) )
let L be non empty multLoopStr_0 ; :: thesis: for a being Element of L holds
( (a | n,L) . (EmptyBag n) = a & ( for b being bag of n st b <> EmptyBag n holds
(a | n,L) . b = 0. L ) )
let a be Element of L; :: thesis: ( (a | n,L) . (EmptyBag n) = a & ( for b being bag of n st b <> EmptyBag n holds
(a | n,L) . b = 0. L ) )
set Z = 0_ n,L;
A1: 0_ n,L = (Bags n) --> (0. L) by POLYNOM1:def 24;
then dom (0_ n,L) = Bags n by FUNCOP_1:19;
hence (a | n,L) . (EmptyBag n) = a by FUNCT_7:33; :: thesis: for b being bag of n st b <> EmptyBag n holds
(a | n,L) . b = 0. L
let b be bag of n; :: thesis: ( b <> EmptyBag n implies (a | n,L) . b = 0. L )
A2: b in Bags n by PRE_POLY:def 12;
assume b <> EmptyBag n ; :: thesis: (a | n,L) . b = 0. L
hence (a | n,L) . b = (0_ n,L) . b by FUNCT_7:34
.= 0. L by A1, A2, FUNCOP_1:13 ;
:: thesis: verum