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₁[ 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₁[p] holds
S₁[p ^ <*n*>]

proof

let p be FinSequence of INT ; :: thesis: for n being Element of INT st S₁[p] holds
S₁[p ^ <*n*>]
let i be Element of INT ; :: thesis: ( S₁[p] implies S₁[p ^ <*i*>] )
set p1 = p ^ <*i*>;
assume A2: S₁[p] ; :: thesis: S₁[p ^ <*i*>]
S₁[p ^ <*i*>]

proof

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 )

proof

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;

A6: len (p ^ <*i*>) in dom (p ^ <*i*>) by FINSEQ_5:6;
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;

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;

suppose ( Product p = 0 & 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 = 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;

end;

end;

hence S₁[p ^ <*i*>] ; :: thesis: verum

end;

A9: S₁[ <*> INT] by RVSUM_1:94;
for p being FinSequence of INT holds S₁[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