let p be non empty FinSequence; :: thesis: for x being object
for n being Element of dom (p ^ <*x*>) holds
( not n <= (len (p ^ <*x*>)) - 1 or n = (len (p ^ <*x*>)) - 1 or n <= (len p) - 1 )
let x be object ; :: thesis: for n being Element of dom (p ^ <*x*>) holds
( not n <= (len (p ^ <*x*>)) - 1 or n = (len (p ^ <*x*>)) - 1 or n <= (len p) - 1 )
let n be Element of dom (p ^ <*x*>); :: thesis: ( not n <= (len (p ^ <*x*>)) - 1 or n = (len (p ^ <*x*>)) - 1 or n <= (len p) - 1 )
A1: len (p ^ <*x*>) = (len p) + (len <*x*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:39 ;
assume A2: n <= (len (p ^ <*x*>)) - 1 ; :: thesis: ( n = (len (p ^ <*x*>)) - 1 or n <= (len p) - 1 )
assume not n = (len (p ^ <*x*>)) - 1 ; :: thesis: n <= (len p) - 1
then A3: n < ((len p) - 1) + 1 by A1, A2, XXREAL_0:1;
(len p) - 1 is Nat by CHORD:1;
hence n <= (len p) - 1 by A3, NAT_1:13; :: thesis: verum