let g be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st g is being_S-Seq & i + 1 < len g holds
g /^ i is being_S-Seq
let i be Nat; :: thesis: ( g is being_S-Seq & i + 1 < len g implies g /^ i is being_S-Seq )
assume that
A1: g is being_S-Seq and
A2: i + 1 < len g ; :: thesis: g /^ i is being_S-Seq
A3: mid (g,(i + 1),(len g)) = g /^ ((i + 1) -' 1) by A2, FINSEQ_6:117
.= g /^ i by NAT_D:34 ;
A4: 1 <= i + 1 by NAT_1:11;
then 1 < len g by A2, XXREAL_0:2;
hence g /^ i is being_S-Seq by A1, A2, A4, A3, JORDAN3:6; :: thesis: verum