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;

now

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 Element of 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 Element of NAT : j + n <= k } & (inferior_realsequence seq) . (j + n) = inf Y3 ) by Def6;

now

let x be set ; :: thesis: ( x in { (seq . k) where k is Element of NAT : j + n <= k } implies x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } )
assume x in { (seq . k) where k is Element of NAT : j + n <= k } ; :: thesis: x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 }
then consider k being Element of 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 Element of NAT : n <= k2 } by A5; :: thesis: verum

end;

then A6: { (seq . k) where k is Element of NAT : j + n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } )
assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; :: thesis: x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 }
then consider k being Element of 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 Element of NAT : j + n <= k1 } by A7; :: thesis: verum

end;

then { (seq . (j + k)) where k is Element of NAT : n <= k } c= { (seq . k) where k is Element of NAT : j + n <= k } by TARSKI:def 3;
then A9: { (seq . (j + k)) where k is Element of NAT : n <= k } = { (seq . k) where k is Element of NAT : j + n <= k } by A6, XBOOLE_0:def 10;

now

let x be set ; :: thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } )
assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; :: thesis: x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 }
then consider k being Element of 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 Element of NAT : n <= k1 } by A11; :: thesis: verum

end;

then A12: { (seq . (j + k)) where k is Element of NAT : n <= k } c= { ((seq ^\ j) . k) where k is Element of NAT : n <= k } by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } implies x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } )
assume x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } ; :: thesis: x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 }
then consider k being Element of 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 Element of NAT : n <= k1 } by A14; :: thesis: verum

end;

then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def 3;
then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } = { (seq . (j + k)) where k is Element of 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;

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