let seq be ExtREAL_sequence; :: thesis: for j being Element of NAT holds

( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq )

let j be Element of NAT ; :: thesis: ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq )

set rseq = seq ^\ j;

hence ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq ) by Th26; :: thesis: verum

( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq )

let j be Element of NAT ; :: thesis: ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq )

set rseq = seq ^\ j;

now :: thesis: for n being Element of NAT holds (inferior_realsequence (seq ^\ j)) . n = ((inferior_realsequence seq) ^\ j) . n

then
(inferior_realsequence seq) ^\ j = inferior_realsequence (seq ^\ j)
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (inferior_realsequence (seq ^\ j)) . n = ((inferior_realsequence seq) ^\ j) . n

A1: ex Y2 being non empty Subset of ExtREAL st

( Y2 = { ((seq ^\ j) . k) where k is Nat : n <= k } & (inferior_realsequence (seq ^\ j)) . n = inf Y2 ) by Def6;

A2: ex Y3 being non empty Subset of ExtREAL st

( Y3 = { (seq . k) where k is Nat : j + n <= k } & (inferior_realsequence seq) . (j + n) = inf Y3 ) by Def6;

then A9: { (seq . (j + k)) where k is Nat : n <= k } = { (seq . k) where k is Nat : j + n <= k } by A6, XBOOLE_0:def 10;

then { ((seq ^\ j) . k) where k is Nat : n <= k } = { (seq . (j + k)) where k is Nat : n <= k } by A12, XBOOLE_0:def 10;

hence (inferior_realsequence (seq ^\ j)) . n = ((inferior_realsequence seq) ^\ j) . n by A1, A2, A9, NAT_1:def 3; :: thesis: verum

end;A1: ex Y2 being non empty Subset of ExtREAL st

( Y2 = { ((seq ^\ j) . k) where k is Nat : n <= k } & (inferior_realsequence (seq ^\ j)) . n = inf Y2 ) by Def6;

A2: ex Y3 being non empty Subset of ExtREAL st

( Y3 = { (seq . k) where k is Nat : j + n <= k } & (inferior_realsequence seq) . (j + n) = inf Y3 ) by Def6;

now :: thesis: for x being object st x in { (seq . k) where k is Nat : j + n <= k } holds

x in { (seq . (j + k2)) where k2 is Nat : n <= k2 }

then A6:
{ (seq . k) where k is Nat : j + n <= k } c= { (seq . (j + k)) where k is Nat : n <= k }
;x in { (seq . (j + k2)) where k2 is Nat : n <= k2 }

let x be object ; :: thesis: ( x in { (seq . k) where k is Nat : j + n <= k } implies x in { (seq . (j + k2)) where k2 is Nat : n <= k2 } )

assume x in { (seq . k) where k is Nat : j + n <= k } ; :: thesis: x in { (seq . (j + k2)) where k2 is Nat : n <= k2 }

then consider k being Nat such that

A3: x = seq . k and

A4: j + n <= k ;

j <= j + n by NAT_1:11;

then reconsider k1 = k - j as Element of NAT by A4, INT_1:5, XXREAL_0:2;

A5: x = seq . (j + k1) by A3;

(j + n) - j <= k - j by A4, XREAL_1:9;

hence x in { (seq . (j + k2)) where k2 is Nat : n <= k2 } by A5; :: thesis: verum

end;assume x in { (seq . k) where k is Nat : j + n <= k } ; :: thesis: x in { (seq . (j + k2)) where k2 is Nat : n <= k2 }

then consider k being Nat such that

A3: x = seq . k and

A4: j + n <= k ;

j <= j + n by NAT_1:11;

then reconsider k1 = k - j as Element of NAT by A4, INT_1:5, XXREAL_0:2;

A5: x = seq . (j + k1) by A3;

(j + n) - j <= k - j by A4, XREAL_1:9;

hence x in { (seq . (j + k2)) where k2 is Nat : n <= k2 } by A5; :: thesis: verum

now :: thesis: for x being object st x in { (seq . (j + k)) where k is Nat : n <= k } holds

x in { (seq . k1) where k1 is Nat : j + n <= k1 }

then
{ (seq . (j + k)) where k is Nat : n <= k } c= { (seq . k) where k is Nat : j + n <= k }
;x in { (seq . k1) where k1 is Nat : j + n <= k1 }

let x be object ; :: thesis: ( x in { (seq . (j + k)) where k is Nat : n <= k } implies x in { (seq . k1) where k1 is Nat : j + n <= k1 } )

assume x in { (seq . (j + k)) where k is Nat : n <= k } ; :: thesis: x in { (seq . k1) where k1 is Nat : j + n <= k1 }

then consider k being Nat such that

A7: x = seq . (j + k) and

A8: n <= k ;

j + n <= j + k by A8, XREAL_1:6;

hence x in { (seq . k1) where k1 is Nat : j + n <= k1 } by A7; :: thesis: verum

end;assume x in { (seq . (j + k)) where k is Nat : n <= k } ; :: thesis: x in { (seq . k1) where k1 is Nat : j + n <= k1 }

then consider k being Nat such that

A7: x = seq . (j + k) and

A8: n <= k ;

j + n <= j + k by A8, XREAL_1:6;

hence x in { (seq . k1) where k1 is Nat : j + n <= k1 } by A7; :: thesis: verum

then A9: { (seq . (j + k)) where k is Nat : n <= k } = { (seq . k) where k is Nat : j + n <= k } by A6, XBOOLE_0:def 10;

now :: thesis: for x being object st x in { (seq . (j + k)) where k is Nat : n <= k } holds

x in { ((seq ^\ j) . k1) where k1 is Nat : n <= k1 }

then A12:
{ (seq . (j + k)) where k is Nat : n <= k } c= { ((seq ^\ j) . k) where k is Nat : n <= k }
;x in { ((seq ^\ j) . k1) where k1 is Nat : n <= k1 }

let x be object ; :: thesis: ( x in { (seq . (j + k)) where k is Nat : n <= k } implies x in { ((seq ^\ j) . k1) where k1 is Nat : n <= k1 } )

assume x in { (seq . (j + k)) where k is Nat : n <= k } ; :: thesis: x in { ((seq ^\ j) . k1) where k1 is Nat : n <= k1 }

then consider k being Nat such that

A10: x = seq . (j + k) and

A11: n <= k ;

x = (seq ^\ j) . k by A10, NAT_1:def 3;

hence x in { ((seq ^\ j) . k1) where k1 is Nat : n <= k1 } by A11; :: thesis: verum

end;assume x in { (seq . (j + k)) where k is Nat : n <= k } ; :: thesis: x in { ((seq ^\ j) . k1) where k1 is Nat : n <= k1 }

then consider k being Nat such that

A10: x = seq . (j + k) and

A11: n <= k ;

x = (seq ^\ j) . k by A10, NAT_1:def 3;

hence x in { ((seq ^\ j) . k1) where k1 is Nat : n <= k1 } by A11; :: thesis: verum

now :: thesis: for x being object st x in { ((seq ^\ j) . k) where k is Nat : n <= k } holds

x in { (seq . (j + k1)) where k1 is Nat : n <= k1 }

then
{ ((seq ^\ j) . k) where k is Nat : n <= k } c= { (seq . (j + k)) where k is Nat : n <= k }
;x in { (seq . (j + k1)) where k1 is Nat : n <= k1 }

let x be object ; :: thesis: ( x in { ((seq ^\ j) . k) where k is Nat : n <= k } implies x in { (seq . (j + k1)) where k1 is Nat : n <= k1 } )

assume x in { ((seq ^\ j) . k) where k is Nat : n <= k } ; :: thesis: x in { (seq . (j + k1)) where k1 is Nat : n <= k1 }

then consider k being Nat such that

A13: x = (seq ^\ j) . k and

A14: n <= k ;

x = seq . (j + k) by A13, NAT_1:def 3;

hence x in { (seq . (j + k1)) where k1 is Nat : n <= k1 } by A14; :: thesis: verum

end;assume x in { ((seq ^\ j) . k) where k is Nat : n <= k } ; :: thesis: x in { (seq . (j + k1)) where k1 is Nat : n <= k1 }

then consider k being Nat such that

A13: x = (seq ^\ j) . k and

A14: n <= k ;

x = seq . (j + k) by A13, NAT_1:def 3;

hence x in { (seq . (j + k1)) where k1 is Nat : n <= k1 } by A14; :: thesis: verum

then { ((seq ^\ j) . k) where k is Nat : n <= k } = { (seq . (j + k)) where k is Nat : n <= k } by A12, XBOOLE_0:def 10;

hence (inferior_realsequence (seq ^\ j)) . n = ((inferior_realsequence seq) ^\ j) . n by A1, A2, A9, NAT_1:def 3; :: thesis: verum

hence ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq ) by Th26; :: thesis: verum