let I be non empty set ; :: thesis: for L being commutative TopGroup
for x being the carrier of b₁ -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)) ) )

A1: now :: thesis: for e being Element of Fin I st e = {} holds
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;

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))

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;

hence 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)) ) ) by A1; :: thesis: verum