let I be non empty set ; for L being commutative TopGroup
for x being the carrier of b1 -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; 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; 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; 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 for e being Element of Fin I st e = {} holds
Product (x,e) = 1_ Llet e be
Element of
Fin I;
( e = {} implies Product (x,e) = 1_ L )assume A2:
e = {}
;
Product (x,e) = 1_ Lconsider 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;
verum end;
now 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;
( e misses f implies Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) )assume A5:
e misses f
;
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;
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; verum