let p be FinSequence; :: thesis: for n being Nat st 1 <= n & n <= len p holds
p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n)
let n be Nat; :: thesis: ( 1 <= n & n <= len p implies p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) )
assume that
A1: 1 <= n and
A2: n <= len p ; :: thesis: p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n)
len p >= (n -' 1) + 1 by A1, A2, XREAL_1:235;
then A3: len p > n -' 1 by NAT_1:13;
p | n = p | ((n -' 1) + 1) by A1, XREAL_1:235
.= (p | (n -' 1)) ^ <*(p . ((n -' 1) + 1))*> by A3, Th83
.= (p | (n -' 1)) ^ <*(p . n)*> by A1, XREAL_1:235 ;
hence p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) by RFINSEQ:8; :: thesis: verum