let h be non constant standard special_circular_sequence; ( 1 <= i_w_n h & i_w_n h <= len (GoB h) & 1 <= i_e_n h & i_e_n h <= len (GoB h) & 1 <= i_w_s h & i_w_s h <= len (GoB h) & 1 <= i_e_s h & i_e_s h <= len (GoB h) )
A1:
[(i_e_n h),(width (GoB h))] in Indices (GoB h)
by Def8;
A2:
[(i_w_s h),1] in Indices (GoB h)
by Def5;
A3:
[(i_e_s h),1] in Indices (GoB h)
by Def6;
[(i_w_n h),(width (GoB h))] in Indices (GoB h)
by Def7;
hence
( 1 <= i_w_n h & i_w_n h <= len (GoB h) & 1 <= i_e_n h & i_e_n h <= len (GoB h) & 1 <= i_w_s h & i_w_s h <= len (GoB h) & 1 <= i_e_s h & i_e_s h <= len (GoB h) )
by A1, A2, A3, MATRIX_0:32; verum