defpred S_{1}[ Nat] means for f being complex-valued FinSequence st len f = $1 & ex i being Nat st

( i in dom f & f . i = 0 ) holds

Product f = 0 ;

let m be complex-valued FinSequence; :: thesis: ( ex i being Nat st

( i in dom m & m . i = 0 ) implies Product m = 0 )

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

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

A15: ex j being Nat st len m = j ;

assume ex i being Nat st

( i in dom m & m . i = 0 ) ; :: thesis: Product m = 0

hence Product m = 0 by A14, A15; :: thesis: verum

( i in dom f & f . i = 0 ) holds

Product f = 0 ;

let m be complex-valued FinSequence; :: thesis: ( ex i being Nat st

( i in dom m & m . i = 0 ) implies Product m = 0 )

A1: for k being Nat st S

S

proof

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

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

_{1}[k + 1]
; :: thesis: verum

end;assume A2: S

now :: thesis: for f being complex-valued FinSequence st len f = k + 1 & ex i being Nat st

( i in dom f & f . i = 0 ) holds

Product f = 0

hence
S( i in dom f & f . i = 0 ) holds

Product f = 0

let f be complex-valued FinSequence; :: thesis: ( len f = k + 1 & ex i being Nat st

( i in dom f & f . i = 0 ) implies Product b_{1} = 0 )

set f1 = f | k;

assume A3: len f = k + 1 ; :: thesis: ( ex i being Nat st

( i in dom f & f . i = 0 ) implies Product b_{1} = 0 )

then A4: len (f | k) = k by FINSEQ_1:59, NAT_1:11;

reconsider f1 = f | k as complex-valued FinSequence ;

f = f1 ^ <*(f . (k + 1))*> by A3, FINSEQ_3:55;

then A5: Product f = (Product f1) * (f . (k + 1)) by RVSUM_1:96;

assume A6: ex i being Nat st

( i in dom f & f . i = 0 ) ; :: thesis: Product b_{1} = 0

end;( i in dom f & f . i = 0 ) implies Product b

set f1 = f | k;

assume A3: len f = k + 1 ; :: thesis: ( ex i being Nat st

( i in dom f & f . i = 0 ) implies Product b

then A4: len (f | k) = k by FINSEQ_1:59, NAT_1:11;

reconsider f1 = f | k as complex-valued FinSequence ;

f = f1 ^ <*(f . (k + 1))*> by A3, FINSEQ_3:55;

then A5: Product f = (Product f1) * (f . (k + 1)) by RVSUM_1:96;

assume A6: ex i being Nat st

( i in dom f & f . i = 0 ) ; :: thesis: Product b

per cases
( f . (k + 1) = 0 or f . (k + 1) <> 0 )
;

end;

suppose A7:
f . (k + 1) <> 0
; :: thesis: Product b_{1} = 0

consider j being Nat such that

A8: j in dom f and

A9: f . j = 0 by A6;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A10: j in Seg (len f) by A8, FINSEQ_1:def 3;

then j <= k + 1 by A3, FINSEQ_1:1;

then j < k + 1 by A7, A9, XXREAL_0:1;

then A11: j <= k by NAT_1:13;

1 <= j by A10, FINSEQ_1:1;

then j in Seg k by A11;

then A12: j in dom f1 by A4, FINSEQ_1:def 3;

then f1 . j = f . j by FUNCT_1:47;

then Product f1 = 0 by A2, A4, A9, A12;

hence Product f = 0 by A5; :: thesis: verum

end;A8: j in dom f and

A9: f . j = 0 by A6;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A10: j in Seg (len f) by A8, FINSEQ_1:def 3;

then j <= k + 1 by A3, FINSEQ_1:1;

then j < k + 1 by A7, A9, XXREAL_0:1;

then A11: j <= k by NAT_1:13;

1 <= j by A10, FINSEQ_1:1;

then j in Seg k by A11;

then A12: j in dom f1 by A4, FINSEQ_1:def 3;

then f1 . j = f . j by FUNCT_1:47;

then Product f1 = 0 by A2, A4, A9, A12;

hence Product f = 0 by A5; :: thesis: verum

proof

A14:
for k being Nat holds S
let f be complex-valued FinSequence; :: thesis: ( len f = 0 & ex i being Nat st

( i in dom f & f . i = 0 ) implies Product f = 0 )

assume len f = 0 ; :: thesis: ( for i being Nat holds

( not i in dom f or not f . i = 0 ) or Product f = 0 )

then Seg (len f) = {} ;

hence ( for i being Nat holds

( not i in dom f or not f . i = 0 ) or Product f = 0 ) by FINSEQ_1:def 3; :: thesis: verum

end;( i in dom f & f . i = 0 ) implies Product f = 0 )

assume len f = 0 ; :: thesis: ( for i being Nat holds

( not i in dom f or not f . i = 0 ) or Product f = 0 )

then Seg (len f) = {} ;

hence ( for i being Nat holds

( not i in dom f or not f . i = 0 ) or Product f = 0 ) by FINSEQ_1:def 3; :: thesis: verum

A15: ex j being Nat st len m = j ;

assume ex i being Nat st

( i in dom m & m . i = 0 ) ; :: thesis: Product m = 0

hence Product m = 0 by A14, A15; :: thesis: verum