let fr be FinSequence of INT ; :: thesis: ( ex d being Nat st

( d in dom fr & not fr . d = 1 & not fr . d = 0 & not fr . d = - 1 ) or Product fr = 1 or Product fr = 0 or Product fr = - 1 )

defpred S_{1}[ FinSequence of INT ] means ( ex d being Nat st

( d in dom $1 & not $1 . d = 1 & not $1 . d = 0 & not $1 . d = - 1 ) or Product $1 = 1 or Product $1 = 0 or Product $1 = - 1 );

A1: for p being FinSequence of INT

for n being Element of INT st S_{1}[p] holds

S_{1}[p ^ <*n*>]
_{1}[ <*> INT]
by RVSUM_1:94;

for p being FinSequence of INT holds S_{1}[p]
from FINSEQ_2:sch 2(A9, A1);

hence ( ex d being Nat st

( d in dom fr & not fr . d = 1 & not fr . d = 0 & not fr . d = - 1 ) or Product fr = 1 or Product fr = 0 or Product fr = - 1 ) ; :: thesis: verum

( d in dom fr & not fr . d = 1 & not fr . d = 0 & not fr . d = - 1 ) or Product fr = 1 or Product fr = 0 or Product fr = - 1 )

defpred S

( d in dom $1 & not $1 . d = 1 & not $1 . d = 0 & not $1 . d = - 1 ) or Product $1 = 1 or Product $1 = 0 or Product $1 = - 1 );

A1: for p being FinSequence of INT

for n being Element of INT st S

S

proof

A9:
S
let p be FinSequence of INT ; :: thesis: for n being Element of INT st S_{1}[p] holds

S_{1}[p ^ <*n*>]

let i be Element of INT ; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*i*>] )

set p1 = p ^ <*i*>;

assume A2: S_{1}[p]
; :: thesis: S_{1}[p ^ <*i*>]

S_{1}[p ^ <*i*>]
_{1}[p ^ <*i*>]
; :: thesis: verum

end;S

let i be Element of INT ; :: thesis: ( S

set p1 = p ^ <*i*>;

assume A2: S

S

proof

hence
S
assume A3:
for d being Nat holds

( not d in dom (p ^ <*i*>) or (p ^ <*i*>) . d = 1 or (p ^ <*i*>) . d = 0 or (p ^ <*i*>) . d = - 1 ) ; :: thesis: ( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )

A4: for d being Nat holds

( not d in dom p or p . d = 1 or p . d = 0 or p . d = - 1 )

A7: Product (p ^ <*i*>) = (Product p) * i by RVSUM_1:96;

len (p ^ <*i*>) = (len p) + 1 by FINSEQ_2:16;

then A8: ( (p ^ <*i*>) . ((len p) + 1) = 1 or (p ^ <*i*>) . ((len p) + 1) = 0 or (p ^ <*i*>) . ((len p) + 1) = - 1 ) by A3, A6;

end;( not d in dom (p ^ <*i*>) or (p ^ <*i*>) . d = 1 or (p ^ <*i*>) . d = 0 or (p ^ <*i*>) . d = - 1 ) ; :: thesis: ( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )

A4: for d being Nat holds

( not d in dom p or p . d = 1 or p . d = 0 or p . d = - 1 )

proof

A6:
len (p ^ <*i*>) in dom (p ^ <*i*>)
by FINSEQ_5:6;
let d be Nat; :: thesis: ( not d in dom p or p . d = 1 or p . d = 0 or p . d = - 1 )

assume A5: d in dom p ; :: thesis: ( p . d = 1 or p . d = 0 or p . d = - 1 )

then ( (p ^ <*i*>) . d = 1 or (p ^ <*i*>) . d = 0 or (p ^ <*i*>) . d = - 1 ) by A3, FINSEQ_2:15;

hence ( p . d = 1 or p . d = 0 or p . d = - 1 ) by A5, FINSEQ_1:def 7; :: thesis: verum

end;assume A5: d in dom p ; :: thesis: ( p . d = 1 or p . d = 0 or p . d = - 1 )

then ( (p ^ <*i*>) . d = 1 or (p ^ <*i*>) . d = 0 or (p ^ <*i*>) . d = - 1 ) by A3, FINSEQ_2:15;

hence ( p . d = 1 or p . d = 0 or p . d = - 1 ) by A5, FINSEQ_1:def 7; :: thesis: verum

A7: Product (p ^ <*i*>) = (Product p) * i by RVSUM_1:96;

len (p ^ <*i*>) = (len p) + 1 by FINSEQ_2:16;

then A8: ( (p ^ <*i*>) . ((len p) + 1) = 1 or (p ^ <*i*>) . ((len p) + 1) = 0 or (p ^ <*i*>) . ((len p) + 1) = - 1 ) by A3, A6;

per cases
( ( Product p = 1 & i = 1 ) or ( Product p = 1 & i = 0 ) or ( Product p = 1 & i = - 1 ) or ( Product p = - 1 & i = 1 ) or ( Product p = - 1 & i = 0 ) or ( Product p = - 1 & i = - 1 ) or ( Product p = 0 & i = 1 ) or ( Product p = 0 & i = 0 ) or ( Product p = 0 & i = - 1 ) )
by A2, A4, A8, FINSEQ_1:42;

end;

suppose
( Product p = 1 & i = 1 )
; :: thesis: ( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )

hence
( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )
by A7; :: thesis: verum

end;suppose
( Product p = 1 & i = 0 )
; :: thesis: ( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )

hence
( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )
by A7; :: thesis: verum

end;suppose
( Product p = 1 & i = - 1 )
; :: thesis: ( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )

hence
( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )
by A7; :: thesis: verum

end;suppose
( Product p = - 1 & i = 1 )
; :: thesis: ( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )

hence
( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )
by A7; :: thesis: verum

end;

suppose
( Product p = - 1 & i = 0 )
; :: thesis: ( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )

hence
( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )
by A7; :: thesis: verum

end;

suppose
( Product p = - 1 & i = - 1 )
; :: thesis: ( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )

hence
( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )
by A7; :: thesis: verum

end;

suppose
( Product p = 0 & i = 1 )
; :: thesis: ( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )

hence
( Product (p ^ <*i*>) = 1 or Product (p ^ <*i*>) = 0 or Product (p ^ <*i*>) = - 1 )
by A7; :: thesis: verum

end;

for p being FinSequence of INT holds S

hence ( ex d being Nat st

( d in dom fr & not fr . d = 1 & not fr . d = 0 & not fr . d = - 1 ) or Product fr = 1 or Product fr = 0 or Product fr = - 1 ) ; :: thesis: verum