let n be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1
let p be Element of D; :: thesis: for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1
let f be FinSequence of D; :: thesis: len (Ins (f,n,p)) = (len f) + 1

per cases ( n <= len f or len f < n ) ;

suppose A1: n <= len f ; :: thesis: len (Ins (f,n,p)) = (len f) + 1

thus len (Ins (f,n,p)) = (len ((f | n) ^ <*p*>)) + (len (f /^ n)) by FINSEQ_1:22
.= (len ((f | n) ^ <*p*>)) + ((len f) - n) by A1, RFINSEQ:def 1
.= ((len (f | n)) + (len <*p*>)) + ((len f) - n) by FINSEQ_1:22
.= ((len (f | n)) + 1) + ((len f) - n) by FINSEQ_1:39
.= (n + 1) + ((len f) - n) by A1, FINSEQ_1:59
.= (len f) + 1 ; :: thesis: verum

end;

suppose len f < n ; :: thesis: len (Ins (f,n,p)) = (len f) + 1

then Ins (f,n,p) = f ^ <*p*> by Th68;
hence len (Ins (f,n,p)) = (len f) + 1 by FINSEQ_2:16; :: thesis: verum

end;

end;