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 8;
then dom (0_ (n,L)) = Bags n ;
hence (a | (n,L)) . (EmptyBag n) = a by FUNCT_7:31; :: 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:32
.= 0. L by A1, A2, FUNCOP_1:7 ;
:: thesis: verum