let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for m being Nat ex M being Real st
( M > 0 & ( for n being Nat st n <= m holds
||.(seq . n).|| < M ) )
let seq be sequence of X; :: thesis: for m being Nat ex M being Real st
( M > 0 & ( for n being Nat st n <= m holds
||.(seq . n).|| < M ) )
defpred S₁[ Nat] means ex M being Real st
( M > 0 & ( for n being Nat st n <= $1 holds
||.(seq . n).|| < M ) );
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
given M1 being Real such that A2: M1 > 0 and
A3: for n being Nat st n <= m holds
||.(seq . n).|| < M1 ; :: thesis: S₁[m + 1]

A4: now :: thesis: ( ||.(seq . (m + 1)).|| >= M1 implies ex M being set st
( M > 0 & ( for n being Nat st n <= m + 1 holds
||.(seq . n).|| < M ) ) )

assume A5: ||.(seq . (m + 1)).|| >= M1 ; :: thesis: ex M being set st
( M > 0 & ( for n being Nat st n <= m + 1 holds
||.(seq . n).|| < M ) )
take M = ||.(seq . (m + 1)).|| + 1; :: thesis: ( M > 0 & ( for n being Nat st n <= m + 1 holds
||.(seq . n).|| < M ) )
M > 0 + 0 by CSSPACE:44, XREAL_1:8;
hence M > 0 ; :: thesis: for n being Nat st n <= m + 1 holds
||.(seq . n).|| < M
let n be Nat; :: thesis: ( n <= m + 1 implies ||.(seq . n).|| < M )
assume A6: n <= m + 1 ; :: thesis: ||.(seq . n).|| < M

A7: now :: thesis: ( m >= n implies ||.(seq . n).|| < M )

assume m >= n ; :: thesis: ||.(seq . n).|| < M
then ||.(seq . n).|| < M1 by A3;
then ||.(seq . n).|| < ||.(seq . (m + 1)).|| by A5, XXREAL_0:2;
then ||.(seq . n).|| + 0 < M by XREAL_1:8;
hence ||.(seq . n).|| < M ; :: thesis: verum

end;

now :: thesis: ( n = m + 1 implies ||.(seq . n).|| < M )

assume n = m + 1 ; :: thesis: ||.(seq . n).|| < M
then ||.(seq . n).|| + 0 < M by XREAL_1:8;
hence ||.(seq . n).|| < M ; :: thesis: verum

end;

hence ||.(seq . n).|| < M by A6, A7, NAT_1:8; :: thesis: verum

end;

now :: thesis: ( ||.(seq . (m + 1)).|| <= M1 implies ex M being set st
( M > 0 & ( for n being Nat st n <= m + 1 holds
||.(seq . n).|| < M ) ) )

assume A8: ||.(seq . (m + 1)).|| <= M1 ; :: thesis: ex M being set st
( M > 0 & ( for n being Nat st n <= m + 1 holds
||.(seq . n).|| < M ) )
take M = M1 + 1; :: thesis: ( M > 0 & ( for n being Nat st n <= m + 1 holds
||.(seq . n).|| < M ) )
thus M > 0 by A2; :: thesis: for n being Nat st n <= m + 1 holds
||.(seq . n).|| < M
let n be Nat; :: thesis: ( n <= m + 1 implies ||.(seq . n).|| < M )
assume A9: n <= m + 1 ; :: thesis: ||.(seq . n).|| < M

A10: now :: thesis: ( m >= n implies ||.(seq . n).|| < M )

assume m >= n ; :: thesis: ||.(seq . n).|| < M
then A11: ||.(seq . n).|| < M1 by A3;
M > M1 + 0 by XREAL_1:8;
hence ||.(seq . n).|| < M by A11, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: ( n = m + 1 implies ||.(seq . n).|| < M )

A12: M > M1 + 0 by XREAL_1:8;
assume n = m + 1 ; :: thesis: ||.(seq . n).|| < M
hence ||.(seq . n).|| < M by A8, A12, XXREAL_0:2; :: thesis: verum

end;

hence ||.(seq . n).|| < M by A9, A10, NAT_1:8; :: thesis: verum

end;

hence S₁[m + 1] by A4; :: thesis: verum

end;

A13: S₁[ 0 ]

proof

take M = ||.(seq . 0).|| + 1; :: thesis: ( M > 0 & ( for n being Nat st n <= 0 holds
||.(seq . n).|| < M ) )
||.(seq . 0).|| + 1 > 0 + 0 by CSSPACE:44, XREAL_1:8;
hence M > 0 ; :: thesis: for n being Nat st n <= 0 holds
||.(seq . n).|| < M
let n be Nat; :: thesis: ( n <= 0 implies ||.(seq . n).|| < M )
assume n <= 0 ; :: thesis: ||.(seq . n).|| < M
then n = 0 ;
then ||.(seq . n).|| + 0 < M by XREAL_1:8;
hence ||.(seq . n).|| < M ; :: thesis: verum

end;

thus for m being Nat holds S₁[m] from NAT_1:sch 2(A13, A1); :: thesis: verum