let X be set ; :: thesis: for A being SetSequence of X holds
( superior_setsequence A = Union_Shift_Seq A & inferior_setsequence A = Intersect_Shift_Seq A )

let A be SetSequence of X; :: thesis:
thus superior_setsequence A = Union_Shift_Seq A :: thesis:
proof
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: . n = () . n
for x being object holds
( x in . n iff x in () . n )
proof
let x be object ; :: thesis: ( x in . n iff x in () . n )
hereby :: thesis: ( x in () . n implies x in . n )
assume x in . n ; :: thesis: x in () . n
then consider k being Nat such that
A1: x in A . (n + k) by SETLIM_1:20;
x in (A ^\ n) . k by ;
then x in Union (A ^\ n) by PROB_1:12;
hence x in () . n by Def7; :: thesis: verum
end;
assume x in () . n ; :: thesis: x in . n
then x in Union (A ^\ n) by Def7;
then consider k being Nat such that
A2: x in (A ^\ n) . k by PROB_1:12;
x in A . (n + k) by ;
hence x in . n by SETLIM_1:20; :: thesis: verum
end;
hence (superior_setsequence A) . n = () . n by TARSKI:2; :: thesis: verum
end;
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis:
for x being object holds
( x in . n iff x in . n )
proof
let x be object ; :: thesis: ( x in . n iff x in . n )
hereby :: thesis: ( x in . n implies x in . n )
assume A3: x in . n ; :: thesis: x in . n
A4: for k being Nat holds x in (A ^\ n) . k
proof
let k be Nat; :: thesis: x in (A ^\ n) . k
x in A . (k + n) by ;
hence x in (A ^\ n) . k by NAT_1:def 3; :: thesis: verum
end;
x in Intersection (A ^\ n) by ;
hence x in . n by Def9; :: thesis: verum
end;
assume x in . n ; :: thesis: x in . n
then A5: x in Intersection (A ^\ n) by Def9;
for k being Nat holds x in A . (n + k)
proof
let k be Nat; :: thesis: x in A . (n + k)
x in (A ^\ n) . k by ;
hence x in A . (n + k) by NAT_1:def 3; :: thesis: verum
end;
hence x in . n by SETLIM_1:19; :: thesis: verum
end;
hence (inferior_setsequence A) . n = . n by TARSKI:2; :: thesis: verum