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 S1[ 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 S1[p] holds
S1[p ^ <*n*>]
proof
let p be FinSequence of INT ; :: thesis: for n being Element of INT st S1[p] holds
S1[p ^ <*n*>]
let i be Element of INT ; :: thesis: ( S1[p] implies S1[p ^ <*i*>] )
set p1 = p ^ <*i*>;
assume A2: S1[p] ; :: thesis: S1[p ^ <*i*>]
S1[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 S1[p ^ <*i*>] ; :: thesis: verum
end;
A9: S1[ <*> INT] by RVSUM_1:94;
for p being FinSequence of INT holds S1[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