let i, j be Nat; for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G holds
h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
let G be Matrix of (TOP-REAL 2); ( G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G implies h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } )
assume that
A1:
G is Y_equal-in-column
and
A2:
1 <= j
and
A3:
j < width G
and
A4:
1 <= i
and
A5:
i <= len G
; h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
A6:
1 <= j + 1
by A2, NAT_1:13;
A7:
j + 1 <= width G
by A3, NAT_1:13;
A8:
(G * (i,j)) `2 = (G * (1,j)) `2
by A1, A2, A3, A4, A5, Th1;
(G * (i,(j + 1))) `2 = (G * (1,(j + 1))) `2
by A1, A4, A5, A6, A7, Th1;
hence
h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }
by A2, A3, A8, Def2; verum