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

for x being object holds

( x in (inferior_setsequence A) . n iff x in (Intersect_Shift_Seq A) . n )

( 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: (inferior_setsequence A) . n = (Intersect_Shift_Seq A) . n
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 object holds

( x in (superior_setsequence A) . n iff x in (Union_Shift_Seq A) . n )

end;for x being object holds

( x in (superior_setsequence A) . n iff x in (Union_Shift_Seq A) . n )

proof

hence
(superior_setsequence A) . n = (Union_Shift_Seq A) . n
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (superior_setsequence A) . n iff x in (Union_Shift_Seq A) . 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 A2, NAT_1:def 3;

hence x in (superior_setsequence A) . n by SETLIM_1:20; :: thesis: verum

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

assume
x in (Union_Shift_Seq A) . n
; :: thesis: x in (superior_setsequence A) . nassume
x in (superior_setsequence A) . n
; :: thesis: x in (Union_Shift_Seq A) . n

then consider k being 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 Def7; :: thesis: verum

end;then consider k being 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 Def7; :: thesis: verum

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 A2, NAT_1:def 3;

hence x in (superior_setsequence A) . n by SETLIM_1:20; :: thesis: verum

for x being object holds

( x in (inferior_setsequence A) . n iff x in (Intersect_Shift_Seq A) . n )

proof

hence
(inferior_setsequence A) . n = (Intersect_Shift_Seq A) . n
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (inferior_setsequence A) . n iff x in (Intersect_Shift_Seq A) . n )

then A5: x in Intersection (A ^\ n) by Def9;

for k being Nat holds x in A . (n + k)

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

assume
x in (Intersect_Shift_Seq A) . n
; :: thesis: x in (inferior_setsequence A) . nassume A3:
x in (inferior_setsequence A) . n
; :: thesis: x in (Intersect_Shift_Seq A) . n

A4: for k being Nat holds x in (A ^\ n) . k

hence x in (Intersect_Shift_Seq A) . n by Def9; :: thesis: verum

end;A4: for k being Nat holds x in (A ^\ n) . k

proof

x in Intersection (A ^\ n)
by A4, PROB_1:13;
let k be 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 A . (k + n) by A3, SETLIM_1:19;

hence x in (A ^\ n) . k by NAT_1:def 3; :: thesis: verum

hence x in (Intersect_Shift_Seq A) . n by Def9; :: thesis: verum

then A5: x in Intersection (A ^\ n) by Def9;

for k being Nat holds x in A . (n + k)

proof

hence
x in (inferior_setsequence A) . n
by SETLIM_1:19; :: thesis: verum
let k be 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;x in (A ^\ n) . k by A5, PROB_1:13;

hence x in A . (n + k) by NAT_1:def 3; :: thesis: verum