defpred S_{1}[ Nat] means for f being FinSequence of F_Complex

for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) & $1 = len f holds

|.(Product f).| = Product g;

set FC = F_Complex ;

set cFC = the carrier of F_Complex;

A1: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
_{1}[i]
from NAT_1:sch 2(A18, A1);

let f be FinSequence of F_Complex; :: thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) holds

|.(Product f).| = Product g

let g be FinSequence of REAL ; :: thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) implies |.(Product f).| = Product g )

assume ( len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) ) ; :: thesis: |.(Product f).| = Product g

hence |.(Product f).| = Product g by A23; :: thesis: verum

for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) & $1 = len f holds

|.(Product f).| = Product g;

set FC = F_Complex ;

set cFC = the carrier of F_Complex;

A1: for i being Nat st S

S

proof

A18:
S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A2: S_{1}[i]
; :: thesis: S_{1}[i + 1]

let f be FinSequence of F_Complex; :: thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) & i + 1 = len f holds

|.(Product f).| = Product g

let g be FinSequence of REAL ; :: thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) & i + 1 = len f implies |.(Product f).| = Product g )

assume that

A3: len f = len g and

A4: for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i and

A5: i + 1 = len f ; :: thesis: |.(Product f).| = Product g

consider g1 being FinSequence of REAL , r being Element of REAL such that

A6: g = g1 ^ <*r*> by A3, A5, FINSEQ_2:19;

A7: len g = (len g1) + (len <*r*>) by A6, FINSEQ_1:22

.= (len g1) + 1 by FINSEQ_1:39 ;

then A8: g . (len f) = r by A3, A6, FINSEQ_1:42;

consider f1 being FinSequence of F_Complex, c being Element of the carrier of F_Complex such that

A9: f = f1 ^ <*c*> by A5, FINSEQ_2:19;

A10: len f = (len f1) + (len <*c*>) by A9, FINSEQ_1:22

.= (len f1) + 1 by FINSEQ_1:39 ;

then A11: dom f1 = dom g1 by A3, A7, FINSEQ_3:29;

A15: Product g = (Product g1) * r by A6, RVSUM_1:96;

reconsider cc = c as Element of COMPLEX by COMPLFLD:def 1;

f <> {} by A5;

then A16: len f in dom f by FINSEQ_5:6;

then f /. (len f) = f . (len f) by PARTFUN1:def 6

.= c by A9, A10, FINSEQ_1:42 ;

then A17: |.cc.| = r by A4, A16, A8;

Product f = (Product f1) * c by A9, GROUP_4:6;

hence |.(Product f).| = |.Pf1.| * |.cc.| by COMPLEX1:65

.= Product g by A2, A3, A5, A15, A10, A7, A12, A17 ;

:: thesis: verum

end;assume A2: S

let f be FinSequence of F_Complex; :: thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) & i + 1 = len f holds

|.(Product f).| = Product g

let g be FinSequence of REAL ; :: thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) & i + 1 = len f implies |.(Product f).| = Product g )

assume that

A3: len f = len g and

A4: for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i and

A5: i + 1 = len f ; :: thesis: |.(Product f).| = Product g

consider g1 being FinSequence of REAL , r being Element of REAL such that

A6: g = g1 ^ <*r*> by A3, A5, FINSEQ_2:19;

A7: len g = (len g1) + (len <*r*>) by A6, FINSEQ_1:22

.= (len g1) + 1 by FINSEQ_1:39 ;

then A8: g . (len f) = r by A3, A6, FINSEQ_1:42;

consider f1 being FinSequence of F_Complex, c being Element of the carrier of F_Complex such that

A9: f = f1 ^ <*c*> by A5, FINSEQ_2:19;

A10: len f = (len f1) + (len <*c*>) by A9, FINSEQ_1:22

.= (len f1) + 1 by FINSEQ_1:39 ;

then A11: dom f1 = dom g1 by A3, A7, FINSEQ_3:29;

A12: now :: thesis: for i being Element of NAT st i in dom f1 holds

|.(f1 /. i).| = g1 . i

reconsider Pf1 = Product f1 as Element of COMPLEX by COMPLFLD:def 1;|.(f1 /. i).| = g1 . i

let i be Element of NAT ; :: thesis: ( i in dom f1 implies |.(f1 /. i).| = g1 . i )

A13: dom f1 c= dom f by A9, FINSEQ_1:26;

assume A14: i in dom f1 ; :: thesis: |.(f1 /. i).| = g1 . i

then f1 /. i = f1 . i by PARTFUN1:def 6

.= f . i by A9, A14, FINSEQ_1:def 7

.= f /. i by A14, A13, PARTFUN1:def 6 ;

hence |.(f1 /. i).| = g . i by A4, A14, A13

.= g1 . i by A6, A11, A14, FINSEQ_1:def 7 ;

:: thesis: verum

end;A13: dom f1 c= dom f by A9, FINSEQ_1:26;

assume A14: i in dom f1 ; :: thesis: |.(f1 /. i).| = g1 . i

then f1 /. i = f1 . i by PARTFUN1:def 6

.= f . i by A9, A14, FINSEQ_1:def 7

.= f /. i by A14, A13, PARTFUN1:def 6 ;

hence |.(f1 /. i).| = g . i by A4, A14, A13

.= g1 . i by A6, A11, A14, FINSEQ_1:def 7 ;

:: thesis: verum

A15: Product g = (Product g1) * r by A6, RVSUM_1:96;

reconsider cc = c as Element of COMPLEX by COMPLFLD:def 1;

f <> {} by A5;

then A16: len f in dom f by FINSEQ_5:6;

then f /. (len f) = f . (len f) by PARTFUN1:def 6

.= c by A9, A10, FINSEQ_1:42 ;

then A17: |.cc.| = r by A4, A16, A8;

Product f = (Product f1) * c by A9, GROUP_4:6;

hence |.(Product f).| = |.Pf1.| * |.cc.| by COMPLEX1:65

.= Product g by A2, A3, A5, A15, A10, A7, A12, A17 ;

:: thesis: verum

proof

A23:
for i being Nat holds S
let f be FinSequence of F_Complex; :: thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) & 0 = len f holds

|.(Product f).| = Product g

let g be FinSequence of REAL ; :: thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) & 0 = len f implies |.(Product f).| = Product g )

assume that

A19: len f = len g and

for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i and

A20: 0 = len f ; :: thesis: |.(Product f).| = Product g

A21: f = <*> the carrier of F_Complex by A20;

then A22: g = <*> the carrier of F_Complex by A19;

Product f = 1r by A21, COMPLFLD:8, GROUP_4:8;

hence |.(Product f).| = Product g by A22, COMPLEX1:48, RVSUM_1:94; :: thesis: verum

end;|.(f /. i).| = g . i ) & 0 = len f holds

|.(Product f).| = Product g

let g be FinSequence of REAL ; :: thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) & 0 = len f implies |.(Product f).| = Product g )

assume that

A19: len f = len g and

for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i and

A20: 0 = len f ; :: thesis: |.(Product f).| = Product g

A21: f = <*> the carrier of F_Complex by A20;

then A22: g = <*> the carrier of F_Complex by A19;

Product f = 1r by A21, COMPLFLD:8, GROUP_4:8;

hence |.(Product f).| = Product g by A22, COMPLEX1:48, RVSUM_1:94; :: thesis: verum

let f be FinSequence of F_Complex; :: thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) holds

|.(Product f).| = Product g

let g be FinSequence of REAL ; :: thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) implies |.(Product f).| = Product g )

assume ( len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) ) ; :: thesis: |.(Product f).| = Product g

hence |.(Product f).| = Product g by A23; :: thesis: verum