let X be RealNormSpace-Sequence; :: thesis: for x being Element of (product X)
for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for y being Point of Y st z = x ^ <*y*> holds
NrProduct z = ||.y.|| * (NrProduct x)
let x be Element of (product X); :: thesis: for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for y being Point of Y st z = x ^ <*y*> holds
NrProduct z = ||.y.|| * (NrProduct x)
let Y be RealNormSpace; :: thesis: for z being Element of (product (X ^ <*Y*>))
for y being Point of Y st z = x ^ <*y*> holds
NrProduct z = ||.y.|| * (NrProduct x)
let z be Element of (product (X ^ <*Y*>)); :: thesis: for y being Point of Y st z = x ^ <*y*> holds
NrProduct z = ||.y.|| * (NrProduct x)
let y be Point of Y; :: thesis: ( z = x ^ <*y*> implies NrProduct z = ||.y.|| * (NrProduct x) )
assume A1: z = x ^ <*y*> ; :: thesis: NrProduct z = ||.y.|| * (NrProduct x)
consider nz being FinSequence of REAL such that
A2: ( dom nz = dom (X ^ <*Y*>) & ( for i being Element of dom (X ^ <*Y*>) holds nz . i = ||.(z . i).|| ) & NrProduct z = Product nz ) by LOPBAN10:def 9;
set nx = nz | (len x);
A3: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
set CX = carr X;
consider x1 being Function such that
A4: ( x = x1 & dom x1 = dom (carr X) & ( for i being object st i in dom (carr X) holds
x1 . i in (carr X) . i ) ) by A3, CARD_3:def 5;
A5: dom x1 = Seg (len (carr X)) by A4, FINSEQ_1:def 3;
reconsider x1 = x1 as FinSequence by A4;
A6: len x = len (carr X) by A4, A5, FINSEQ_1:def 3
.= len X by PRVECT_1:def 11 ;
dom nz = Seg (len (X ^ <*Y*>)) by A2, FINSEQ_1:def 3;
then A7: len nz = len (X ^ <*Y*>) by FINSEQ_1:def 3
.= (len X) + (len <*Y*>) by FINSEQ_1:22
.= (len X) + 1 by FINSEQ_1:40 ;
then A8: len (nz | (len x)) = len x by NAT_1:11, A6, FINSEQ_1:59;
A9: len (X ^ <*Y*>) = (len X) + (len <*Y*>) by FINSEQ_1:22
.= (len X) + 1 by FINSEQ_1:40 ;
A10: dom x = Seg (len x) by FINSEQ_1:def 3
.= dom X by A6, FINSEQ_1:def 3 ;
A11: dom nz = Seg ((len X) + 1) by A7, FINSEQ_1:def 3
.= dom (X ^ <*Y*>) by A9, FINSEQ_1:def 3 ;
A12: len nz = (len (nz | (len x))) + 1 by A6, A7, NAT_1:11, FINSEQ_1:59;
A13: dom (nz | (len x)) = Seg (len x) by A8, FINSEQ_1:def 3
.= dom X by A6, FINSEQ_1:def 3 ;
A14: for i being Element of dom X holds (nz | (len x)) . i = ||.(x . i).||

proof

let i be Element of dom X; :: thesis: (nz | (len x)) . i = ||.(x . i).||
i in dom X ;
then A15: i in Seg (len X) by FINSEQ_1:def 3;
then A16: ( 1 <= i & i <= len X ) by FINSEQ_1:1;
len X <= (len X) + 1 by NAT_1:11;
then i <= (len X) + 1 by A16, XXREAL_0:2;
then i in Seg ((len X) + 1) by A16;
then reconsider j = i as Element of dom (X ^ <*Y*>) by A9, FINSEQ_1:def 3;
A17: (X ^ <*Y*>) . i = X . i by FINSEQ_1:def 7;
thus (nz | (len x)) . i = nz . i by A6, A15, FUNCT_1:49
.= ||.(z . j).|| by A2
.= ||.(x . i).|| by A1, A10, A17, FINSEQ_1:def 7 ; :: thesis: verum

end;

0 <= Product (nz | (len x))

proof

per cases ( ex i being Nat st
( i in dom (nz | (len x)) & (nz | (len x)) . i = 0 ) or for i being Nat holds
( not i in dom (nz | (len x)) or not (nz | (len x)) . i = 0 ) ) ;

suppose ex i being Nat st
( i in dom (nz | (len x)) & (nz | (len x)) . i = 0 ) ; :: thesis: 0 <= Product (nz | (len x))

hence 0 <= Product (nz | (len x)) by RVSUM_1:103; :: thesis: verum

end;

suppose A18: for i being Nat holds
( not i in dom (nz | (len x)) or not (nz | (len x)) . i = 0 ) ; :: thesis: 0 <= Product (nz | (len x))

for i being Element of NAT st i in dom (nz | (len x)) holds
(nz | (len x)) . i > 0

proof

let i be Element of NAT ; :: thesis: ( i in dom (nz | (len x)) implies (nz | (len x)) . i > 0 )
assume A19: i in dom (nz | (len x)) ; :: thesis: (nz | (len x)) . i > 0
reconsider i1 = i as Element of dom X by A13, A19;
A20: 0 <= ||.(x . i1).|| by NORMSP_1:4;
(nz | (len x)) . i = ||.(x . i1).|| by A14;
hence (nz | (len x)) . i > 0 by A18, A19, A20, XXREAL_0:1; :: thesis: verum

end;

hence 0 <= Product (nz | (len x)) by NAT_4:42; :: thesis: verum

end;

end;

end;

then not Product (nz | (len x)) is negative by XXREAL_0:def 7;
then A21: NrProduct x = Product (nz | (len x)) by A13, A14, LOPBAN10:def 9;
A22: len ((nz | (len x)) ^ <*||.y.||*>) = (len (nz | (len x))) + (len <*||.y.||*>) by FINSEQ_1:22
.= (len X) + (len <*||.y.||*>) by A6, A7, NAT_1:11, FINSEQ_1:59
.= (len X) + 1 by FINSEQ_1:40 ;
A23: dom ((nz | (len x)) ^ <*||.y.||*>) = Seg ((len X) + 1) by A22, FINSEQ_1:def 3
.= dom nz by A7, FINSEQ_1:def 3 ;
for i being object st i in dom ((nz | (len x)) ^ <*||.y.||*>) holds
((nz | (len x)) ^ <*||.y.||*>) . i = nz . i

proof

let i be object ; :: thesis: ( i in dom ((nz | (len x)) ^ <*||.y.||*>) implies ((nz | (len x)) ^ <*||.y.||*>) . i = nz . i )
assume A24: i in dom ((nz | (len x)) ^ <*||.y.||*>) ; :: thesis: ((nz | (len x)) ^ <*||.y.||*>) . i = nz . i
then A25: i in Seg (len nz) by A23, FINSEQ_1:def 3;
reconsider i1 = i as Nat by A24;

per cases ( i1 <= len (nz | (len x)) or len (nz | (len x)) < i1 ) ;

suppose A26: i1 <= len (nz | (len x)) ; :: thesis: ((nz | (len x)) ^ <*||.y.||*>) . i = nz . i

A27: ( 1 <= i1 & i1 <= (len (nz | (len x))) + 1 ) by A12, A25, FINSEQ_1:1;
then A28: i1 in Seg (len (nz | (len x))) by A26;
reconsider i2 = i1 as Element of dom X by A6, A8, A28, FINSEQ_1:def 3;
A29: i2 in dom (nz | (len x)) by A28, FINSEQ_1:def 3;
A30: i2 in Seg (len X) by A6, A8, A26, A27;
((nz | (len x)) ^ <*||.y.||*>) . i2 = (nz | (len x)) . i1 by A29, FINSEQ_1:def 7
.= nz . i2 by A6, A30, FUNCT_1:49 ;
hence ((nz | (len x)) ^ <*||.y.||*>) . i = nz . i ; :: thesis: verum

end;

suppose len (nz | (len x)) < i1 ; :: thesis: ((nz | (len x)) ^ <*||.y.||*>) . i = nz . i

then A31: (len (nz | (len x))) + 1 <= i1 by NAT_1:13;
( 1 <= i1 & i1 <= (len (nz | (len x))) + 1 ) by A25, FINSEQ_1:1, A12;
then A32: i1 = (len (nz | (len x))) + 1 by A31, XXREAL_0:1;
reconsider i2 = i1 as Element of dom (X ^ <*Y*>) by A11, A23, A24;
A33: (X ^ <*Y*>) . i2 = Y by A6, A8, A32, FINSEQ_1:42;
nz . i2 = ||.(z . i2).|| by A2
.= ||.y.|| by A1, A8, A32, A33, FINSEQ_1:42 ;
hence ((nz | (len x)) ^ <*||.y.||*>) . i = nz . i by FINSEQ_1:42, A32; :: thesis: verum

end;

end;

end;

then (nz | (len x)) ^ <*||.y.||*> = nz by A23, FUNCT_1:2;
hence NrProduct z = ||.y.|| * (NrProduct x) by A2, A21, RVSUM_1:96; :: thesis: verum