let I be non empty set ; :: thesis: for L being commutative TopGroup

for x being the carrier of b_{1} -valued ManySortedSet of I

for J, e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

let L be commutative TopGroup; :: thesis: for x being the carrier of L -valued ManySortedSet of I

for J, e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

let x be the carrier of L -valued ManySortedSet of I; :: thesis: for J, e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

let J be Element of Fin I; :: thesis: for e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) ) by A1; :: thesis: verum

for x being the carrier of b

for J, e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

let L be commutative TopGroup; :: thesis: for x being the carrier of L -valued ManySortedSet of I

for J, e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

let x be the carrier of L -valued ManySortedSet of I; :: thesis: for J, e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

let J be Element of Fin I; :: thesis: for e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

A1: now :: thesis: for e being Element of Fin I st e = {} holds

Product (x,e) = 1_ L

Product (x,e) = 1_ L

let e be Element of Fin I; :: thesis: ( e = {} implies Product (x,e) = 1_ L )

assume A2: e = {} ; :: thesis: Product (x,e) = 1_ L

consider p being one-to-one FinSequence of I such that

A3: rng p = e and

A4: Product (x,e) = the multF of L "**" (# (p,x)) by Def2;

p = {} by A3, A2;

then ( # (p,x) = {} & the multF of L is having_a_unity & len (# (p,x)) = 0 ) ;

then Product (x,e) = the_unity_wrt the multF of L by A4, FINSOP_1:def 1;

hence Product (x,e) = 1_ L by GROUP_1:22; :: thesis: verum

end;assume A2: e = {} ; :: thesis: Product (x,e) = 1_ L

consider p being one-to-one FinSequence of I such that

A3: rng p = e and

A4: Product (x,e) = the multF of L "**" (# (p,x)) by Def2;

p = {} by A3, A2;

then ( # (p,x) = {} & the multF of L is having_a_unity & len (# (p,x)) = 0 ) ;

then Product (x,e) = the_unity_wrt the multF of L by A4, FINSOP_1:def 1;

hence Product (x,e) = 1_ L by GROUP_1:22; :: thesis: verum

now :: thesis: for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f))

hence
for e being Element of Fin I st e = {} holds Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f))

let e, f be Element of Fin I; :: thesis: ( e misses f implies Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) )

assume A5: e misses f ; :: thesis: Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f))

consider pe being one-to-one FinSequence of I such that

A6: rng pe = e and

A7: Product (x,e) = the multF of L "**" (# (pe,x)) by Def2;

consider pf being one-to-one FinSequence of I such that

A8: rng pf = f and

A9: Product (x,f) = the multF of L "**" (# (pf,x)) by Def2;

reconsider pepf = pe ^ pf as one-to-one FinSequence of I by A5, A6, A8, FINSEQ_3:91;

A10: # (pepf,x) = (# (pe,x)) ^ (# (pf,x)) by Th3;

rng pepf = e \/ f by A6, A8, FINSEQ_1:31;

then Product (x,(e \/ f)) = the multF of L "**" (# (pepf,x)) by Def2;

hence Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) by A7, A9, A10, FINSOP_1:5; :: thesis: verum

end;assume A5: e misses f ; :: thesis: Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f))

consider pe being one-to-one FinSequence of I such that

A6: rng pe = e and

A7: Product (x,e) = the multF of L "**" (# (pe,x)) by Def2;

consider pf being one-to-one FinSequence of I such that

A8: rng pf = f and

A9: Product (x,f) = the multF of L "**" (# (pf,x)) by Def2;

reconsider pepf = pe ^ pf as one-to-one FinSequence of I by A5, A6, A8, FINSEQ_3:91;

A10: # (pepf,x) = (# (pe,x)) ^ (# (pf,x)) by Th3;

rng pepf = e \/ f by A6, A8, FINSEQ_1:31;

then Product (x,(e \/ f)) = the multF of L "**" (# (pepf,x)) by Def2;

hence Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) by A7, A9, A10, FINSOP_1:5; :: thesis: verum

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) ) by A1; :: thesis: verum