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

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