let p be non empty FinSequence; :: thesis: for x being object
for n being Element of dom (<*x*> ^ p) holds
( not n <= (len (<*x*> ^ p)) - 1 or n = 1 or ( n - 1 in dom p & n - 1 <= (len p) - 1 ) )
let x be object ; :: thesis: for n being Element of dom (<*x*> ^ p) holds
( not n <= (len (<*x*> ^ p)) - 1 or n = 1 or ( n - 1 in dom p & n - 1 <= (len p) - 1 ) )
let n be Element of dom (<*x*> ^ p); :: thesis: ( not n <= (len (<*x*> ^ p)) - 1 or n = 1 or ( n - 1 in dom p & n - 1 <= (len p) - 1 ) )
A1: len (<*x*> ^ p) = (len <*x*>) + (len p) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:39 ;
assume n <= (len (<*x*> ^ p)) - 1 ; :: thesis: ( n = 1 or ( n - 1 in dom p & n - 1 <= (len p) - 1 ) )
then A2: n - 1 <= (len p) - 1 by A1, XREAL_1:9;
then A3: (n - 1) + 0 <= ((len p) - 1) + 1 by XREAL_1:7;
assume A4: n <> 1 ; :: thesis: ( n - 1 in dom p & n - 1 <= (len p) - 1 )
not n is zero by FINSEQ_3:25;
then A5: n - 1 is Nat by INT_1:74;
1 <= n - 1

proof

assume not 1 <= n - 1 ; :: thesis: contradiction
then n - 1 = 0 by A5, NAT_1:14;
hence contradiction by A4; :: thesis: verum

end;

hence n - 1 in dom p by A3, A5, FINSEQ_3:25; :: thesis: n - 1 <= (len p) - 1
thus n - 1 <= (len p) - 1 by A2; :: thesis: verum