let n be Element of NAT ; :: thesis: for p, q being FinSequence of NAT holds len ((<*n*> ^ p) ^ q) = (1 + (len p)) + (len q)
let p, q be FinSequence of NAT ; :: thesis: len ((<*n*> ^ p) ^ q) = (1 + (len p)) + (len q)
len (p ^ q) = (len p) + (len q) by FINSEQ_1:22;
then A1: (len <*n*>) + (len (p ^ q)) = ((len <*n*>) + (len p)) + (len q) ;
len ((<*n*> ^ p) ^ q) = len (<*n*> ^ (p ^ q)) by FINSEQ_1:32
.= (len <*n*>) + (len (p ^ q)) by FINSEQ_1:22 ;
hence len ((<*n*> ^ p) ^ q) = (1 + (len p)) + (len q) by A1, FINSEQ_1:40; :: thesis: verum