let p be FinSequence; :: thesis: for x being object
for n being Nat st x in rng p & n in dom (p |-- x) holds
n + (x .. p) in dom p
let x be object ; :: thesis: for n being Nat st x in rng p & n in dom (p |-- x) holds
n + (x .. p) in dom p
let n be Nat; :: thesis: ( x in rng p & n in dom (p |-- x) implies n + (x .. p) in dom p )
assume that
A1: x in rng p and
A2: n in dom (p |-- x) ; :: thesis: n + (x .. p) in dom p
reconsider m = (len p) - (x .. p) as Element of NAT by A1, Th22;
n in Seg m by A1, A2, Th42;
then n <= (len p) - (x .. p) by FINSEQ_1:1;
then A3: n + (x .. p) <= len p by XREAL_1:19;
1 <= n by A2, FINSEQ_3:25;
then 1 <= n + (x .. p) by NAT_1:12;
hence n + (x .. p) in dom p by A3, FINSEQ_3:25; :: thesis: verum