let N1, N2 be non negative Real; :: thesis: ( ex Nx being FinSequence of REAL st
( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & N1 = Product Nx ) & ex Nx being FinSequence of REAL st
( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & N2 = Product Nx ) implies N1 = N2 )
given Nx1 being FinSequence of REAL such that A21: ( dom Nx1 = dom X & ( for i being Element of dom X holds Nx1 . i = ||.(x . i).|| ) & N1 = Product Nx1 ) ; :: thesis: ( for Nx being FinSequence of REAL holds
( not dom Nx = dom X or ex i being Element of dom X st not Nx . i = ||.(x . i).|| or not N2 = Product Nx ) or N1 = N2 )
given Nx2 being FinSequence of REAL such that A22: ( dom Nx2 = dom X & ( for i being Element of dom X holds Nx2 . i = ||.(x . i).|| ) & N2 = Product Nx2 ) ; :: thesis: N1 = N2
for i being Nat st i in dom Nx1 holds
Nx1 . i = Nx2 . i
proof
let k be Nat; :: thesis: ( k in dom Nx1 implies Nx1 . k = Nx2 . k )
assume k in dom Nx1 ; :: thesis: Nx1 . k = Nx2 . k
then reconsider i = k as Element of dom X by A21;
Nx1 . i = ||.(x . i).|| by A21;
hence Nx1 . k = Nx2 . k by A22; :: thesis: verum
end;
then Nx1 = Nx2 by A21, A22;
hence N1 = N2 by A21, A22; :: thesis: verum