defpred S_{1}[ Nat] means for b being FinSequence of INT st len b = $1 holds

ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) );

A1: S_{1}[ 0 ]
_{1}[k] holds

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

hence for b being FinSequence of INT ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) ; :: thesis: verum

ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) );

A1: S

proof

A7:
for k being Nat st S
let b be FinSequence of INT ; :: thesis: ( len b = 0 implies ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) )

assume A2: len b = 0 ; :: thesis: ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) )

A3: 1 in INT by INT_1:def 2;

rng <*1*> = {1} by FINSEQ_1:39;

then rng <*1*> c= INT by A3, ZFMISC_1:31;

then reconsider m = <*1*> as non empty FinSequence of INT by FINSEQ_1:def 4;

A4: len m = (len b) + 1 by A2, FINSEQ_1:40;

A5: m . 1 = 1 by FINSEQ_1:40;

A6: for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) by A2;

b = <*> REAL by A2;

hence ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by A4, A5, A6, RVSUM_1:94; :: thesis: verum

end;( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) )

assume A2: len b = 0 ; :: thesis: ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) )

A3: 1 in INT by INT_1:def 2;

rng <*1*> = {1} by FINSEQ_1:39;

then rng <*1*> c= INT by A3, ZFMISC_1:31;

then reconsider m = <*1*> as non empty FinSequence of INT by FINSEQ_1:def 4;

A4: len m = (len b) + 1 by A2, FINSEQ_1:40;

A5: m . 1 = 1 by FINSEQ_1:40;

A6: for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) by A2;

b = <*> REAL by A2;

hence ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by A4, A5, A6, RVSUM_1:94; :: thesis: verum

S

proof

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

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

let b be FinSequence of INT ; :: thesis: ( len b = k + 1 implies ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) )

assume A9: len b = k + 1 ; :: thesis: ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) )

set b1 = b | k;

A10: len (b | k) = k by A9, FINSEQ_1:59, NAT_1:12;

then consider m1 being non empty FinSequence of INT such that

A11: ( (len (b | k)) + 1 = len m1 & m1 . 1 = 1 & ( for i being Nat st 1 <= i & i <= len (b | k) holds

m1 . (i + 1) = (m1 . i) * ((b | k) . i) ) & Product (b | k) = m1 . ((len (b | k)) + 1) ) by A8;

set m = m1 ^ <*((Product (b | k)) * (b . (len b)))*>;

A12: (Product (b | k)) * (b . (len b)) in INT by A11, INT_1:def 2;

A13: rng <*((Product (b | k)) * (b . (len b)))*> = {((Product (b | k)) * (b . (len b)))} by FINSEQ_1:39;

then A14: rng <*((Product (b | k)) * (b . (len b)))*> c= INT by A12, ZFMISC_1:31;

A15: len (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (len m1) + (len <*((Product (b | k)) * (b . (len b)))*>) by FINSEQ_1:22

.= ((len (b | k)) + 1) + 1 by A11, FINSEQ_1:40

.= (len b) + 1 by A9, FINSEQ_1:59, NAT_1:12 ;

A16: rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (rng m1) \/ {((Product (b | k)) * (b . (len b)))} by A13, FINSEQ_1:31;

rng m1 c= INT by FINSEQ_1:def 4;

then rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) c= INT by A13, A16, A14, XBOOLE_1:8;

then reconsider m = m1 ^ <*((Product (b | k)) * (b . (len b)))*> as non empty FinSequence of INT by FINSEQ_1:def 4;

A17: len m1 = k + 1 by A9, FINSEQ_1:59, NAT_1:12, A11;

( 1 <= 1 & 1 <= k + 1 ) by NAT_1:12;

then 1 in dom m1 by A17, FINSEQ_3:25;

then A18: m . 1 = 1 by A11, FINSEQ_1:def 7;

A19: for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i)

then A32: b = (b | k) ^ <*(b . (len b))*> by A9, FINSEQ_1:58;

len b in Seg (len m1) by A9, A17, FINSEQ_1:4;

then A33: len b in dom m1 by FINSEQ_1:def 3;

A34: ( 1 <= len b & len b <= len b ) by A9, NAT_1:12;

Product b = (m1 . ((len (b | k)) + 1)) * (b . (len b)) by A11, A32, RVSUM_1:96

.= (m1 . (len b)) * (b . (len b)) by A9, FINSEQ_1:59, NAT_1:12

.= (m . (len b)) * (b . (len b)) by A33, FINSEQ_1:def 7

.= m . ((len b) + 1) by A19, A34 ;

hence ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by A15, A18, A19; :: thesis: verum

end;assume A8: S

let b be FinSequence of INT ; :: thesis: ( len b = k + 1 implies ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) )

assume A9: len b = k + 1 ; :: thesis: ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) )

set b1 = b | k;

A10: len (b | k) = k by A9, FINSEQ_1:59, NAT_1:12;

then consider m1 being non empty FinSequence of INT such that

A11: ( (len (b | k)) + 1 = len m1 & m1 . 1 = 1 & ( for i being Nat st 1 <= i & i <= len (b | k) holds

m1 . (i + 1) = (m1 . i) * ((b | k) . i) ) & Product (b | k) = m1 . ((len (b | k)) + 1) ) by A8;

set m = m1 ^ <*((Product (b | k)) * (b . (len b)))*>;

A12: (Product (b | k)) * (b . (len b)) in INT by A11, INT_1:def 2;

A13: rng <*((Product (b | k)) * (b . (len b)))*> = {((Product (b | k)) * (b . (len b)))} by FINSEQ_1:39;

then A14: rng <*((Product (b | k)) * (b . (len b)))*> c= INT by A12, ZFMISC_1:31;

A15: len (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (len m1) + (len <*((Product (b | k)) * (b . (len b)))*>) by FINSEQ_1:22

.= ((len (b | k)) + 1) + 1 by A11, FINSEQ_1:40

.= (len b) + 1 by A9, FINSEQ_1:59, NAT_1:12 ;

A16: rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (rng m1) \/ {((Product (b | k)) * (b . (len b)))} by A13, FINSEQ_1:31;

rng m1 c= INT by FINSEQ_1:def 4;

then rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) c= INT by A13, A16, A14, XBOOLE_1:8;

then reconsider m = m1 ^ <*((Product (b | k)) * (b . (len b)))*> as non empty FinSequence of INT by FINSEQ_1:def 4;

A17: len m1 = k + 1 by A9, FINSEQ_1:59, NAT_1:12, A11;

( 1 <= 1 & 1 <= k + 1 ) by NAT_1:12;

then 1 in dom m1 by A17, FINSEQ_3:25;

then A18: m . 1 = 1 by A11, FINSEQ_1:def 7;

A19: for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i)

proof

b | (k + 1) = (b | k) ^ <*(b . (len b))*>
by A9, INT_6:5;
let i be Nat; :: thesis: ( 1 <= i & i <= len b implies m . (i + 1) = (m . i) * (b . i) )

assume A20: ( 1 <= i & i <= len b ) ; :: thesis: m . (i + 1) = (m . i) * (b . i)

end;assume A20: ( 1 <= i & i <= len b ) ; :: thesis: m . (i + 1) = (m . i) * (b . i)

per cases
( i = len b or i <> len b )
;

end;

suppose A21:
i = len b
; :: thesis: m . (i + 1) = (m . i) * (b . i)

(len (b | k)) + 1 in Seg (len m1)
by A10, A17, FINSEQ_1:4;

then (len (b | k)) + 1 in dom m1 by FINSEQ_1:def 3;

then A22: m1 . ((len (b | k)) + 1) = m . ((len (b | k)) + 1) by FINSEQ_1:def 7

.= m . i by A9, A21, FINSEQ_1:59, NAT_1:12 ;

1 in Seg 1 ;

then A23: 1 in dom <*((Product (b | k)) * (b . (len b)))*> by FINSEQ_1:38;

thus m . (i + 1) = <*((Product (b | k)) * (b . (len b)))*> . 1 by A21, A9, A17, A23, FINSEQ_1:def 7

.= (m . i) * (b . i) by A22, A21, A11, FINSEQ_1:40 ; :: thesis: verum

end;then (len (b | k)) + 1 in dom m1 by FINSEQ_1:def 3;

then A22: m1 . ((len (b | k)) + 1) = m . ((len (b | k)) + 1) by FINSEQ_1:def 7

.= m . i by A9, A21, FINSEQ_1:59, NAT_1:12 ;

1 in Seg 1 ;

then A23: 1 in dom <*((Product (b | k)) * (b . (len b)))*> by FINSEQ_1:38;

thus m . (i + 1) = <*((Product (b | k)) * (b . (len b)))*> . 1 by A21, A9, A17, A23, FINSEQ_1:def 7

.= (m . i) * (b . i) by A22, A21, A11, FINSEQ_1:40 ; :: thesis: verum

suppose
i <> len b
; :: thesis: m . (i + 1) = (m . i) * (b . i)

then A24:
i < len b
by A20, XXREAL_0:1;

then A25: ( 1 <= i & i <= len (b | k) ) by A10, A9, A20, NAT_1:13;

then A26: m1 . (i + 1) = (m1 . i) * ((b | k) . i) by A11;

i in Seg (len m1) by A20, A9, A17;

then A27: i in dom m1 by FINSEQ_1:def 3;

A28: i + 1 <= len m1 by A9, A17, A24, NAT_1:13;

1 <= i + 1 by NAT_1:12;

then i + 1 in Seg (len m1) by A28;

then A29: i + 1 in dom m1 by FINSEQ_1:def 3;

i in Seg k by A25, A10;

then A30: b . i = (b | k) . i by FUNCT_1:49;

A31: m . i = m1 . i by A27, FINSEQ_1:def 7;

thus m . (i + 1) = (m . i) * (b . i) by A26, A29, A30, A31, FINSEQ_1:def 7; :: thesis: verum

end;then A25: ( 1 <= i & i <= len (b | k) ) by A10, A9, A20, NAT_1:13;

then A26: m1 . (i + 1) = (m1 . i) * ((b | k) . i) by A11;

i in Seg (len m1) by A20, A9, A17;

then A27: i in dom m1 by FINSEQ_1:def 3;

A28: i + 1 <= len m1 by A9, A17, A24, NAT_1:13;

1 <= i + 1 by NAT_1:12;

then i + 1 in Seg (len m1) by A28;

then A29: i + 1 in dom m1 by FINSEQ_1:def 3;

i in Seg k by A25, A10;

then A30: b . i = (b | k) . i by FUNCT_1:49;

A31: m . i = m1 . i by A27, FINSEQ_1:def 7;

thus m . (i + 1) = (m . i) * (b . i) by A26, A29, A30, A31, FINSEQ_1:def 7; :: thesis: verum

then A32: b = (b | k) ^ <*(b . (len b))*> by A9, FINSEQ_1:58;

len b in Seg (len m1) by A9, A17, FINSEQ_1:4;

then A33: len b in dom m1 by FINSEQ_1:def 3;

A34: ( 1 <= len b & len b <= len b ) by A9, NAT_1:12;

Product b = (m1 . ((len (b | k)) + 1)) * (b . (len b)) by A11, A32, RVSUM_1:96

.= (m1 . (len b)) * (b . (len b)) by A9, FINSEQ_1:59, NAT_1:12

.= (m . (len b)) * (b . (len b)) by A33, FINSEQ_1:def 7

.= m . ((len b) + 1) by A19, A34 ;

hence ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by A15, A18, A19; :: thesis: verum

hence for b being FinSequence of INT ex m being non empty FinSequence of INT st

( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds

m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) ; :: thesis: verum