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: ( superior_setsequence A = Union_Shift_Seq A & inferior_setsequence A = Intersect_Shift_Seq A )
thus superior_setsequence A = Union_Shift_Seq A :: thesis: inferior_setsequence A = Intersect_Shift_Seq A

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (superior_setsequence A) . n = (Union_Shift_Seq A) . n
for x being set holds
( x in (superior_setsequence A) . n iff x in (Union_Shift_Seq A) . n )

proof

let x be set ; :: thesis: ( x in (superior_setsequence A) . n iff x in (Union_Shift_Seq A) . n )

hereby :: thesis: ( x in (Union_Shift_Seq A) . n implies x in (superior_setsequence A) . n )

assume x in (superior_setsequence A) . n ; :: thesis: x in (Union_Shift_Seq A) . n
then consider k being Element of NAT such that
A1: x in A . (n + k) by SETLIM_1:20;
x in (A ^\ n) . k by A1, NAT_1:def 3;
then x in Union (A ^\ n) by PROB_1:12;
hence x in (Union_Shift_Seq A) . n by Def9; :: thesis: verum

end;

assume x in (Union_Shift_Seq A) . n ; :: thesis: x in (superior_setsequence A) . n
then x in Union (A ^\ n) by Def9;
then consider k being Element of NAT such that
A2: x in (A ^\ n) . k by PROB_1:12;
x in A . (n + k) by A2, NAT_1:def 3;
hence x in (superior_setsequence A) . n by SETLIM_1:20; :: thesis: verum

end;

hence (superior_setsequence A) . n = (Union_Shift_Seq A) . n by TARSKI:1; :: thesis: verum

end;

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (inferior_setsequence A) . n = (Intersect_Shift_Seq A) . n
for x being set holds
( x in (inferior_setsequence A) . n iff x in (Intersect_Shift_Seq A) . n )

proof

let x be set ; :: thesis: ( x in (inferior_setsequence A) . n iff x in (Intersect_Shift_Seq A) . n )

hereby :: thesis: ( x in (Intersect_Shift_Seq A) . n implies x in (inferior_setsequence A) . n )

assume A3: x in (inferior_setsequence A) . n ; :: thesis: x in (Intersect_Shift_Seq A) . n
A4: for k being Element of NAT holds x in (A ^\ n) . k

proof

let k be Element of NAT ; :: thesis: x in (A ^\ n) . k
x in A . (k + n) by A3, SETLIM_1:19;
hence x in (A ^\ n) . k by NAT_1:def 3; :: thesis: verum

end;

x in Intersection (A ^\ n) by A4, PROB_1:13;
hence x in (Intersect_Shift_Seq A) . n by Def12; :: thesis: verum

end;

assume x in (Intersect_Shift_Seq A) . n ; :: thesis: x in (inferior_setsequence A) . n
then A5: x in Intersection (A ^\ n) by Def12;
for k being Element of NAT holds x in A . (n + k)

proof

let k be Element of NAT ; :: thesis: x in A . (n + k)
x in (A ^\ n) . k by A5, PROB_1:13;
hence x in A . (n + k) by NAT_1:def 3; :: thesis: verum

end;

hence x in (inferior_setsequence A) . n by SETLIM_1:19; :: thesis: verum

end;

hence (inferior_setsequence A) . n = (Intersect_Shift_Seq A) . n by TARSKI:1; :: thesis: verum