let j be Nat; for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds
v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 }
let G be Matrix of (TOP-REAL 2); ( G is V3() & G is X_equal-in-line & 1 <= j & j <= width G implies v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } )
assume that
A1:
( G is V3() & G is X_equal-in-line )
and
A2:
1 <= j
and
A3:
j <= width G
; v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 }
set A = { |[r,s]| where r, s is Real : (G * (1,j)) `1 >= r } ;
A4:
0 <> len G
by A1, MATRIX_0:def 10;
then A5:
0 < len G
;
1 <= len G
by A4, NAT_1:14;
then
(G * (1,j)) `1 = (G * (1,1)) `1
by A1, A2, A3, Th2;
then
{ |[r,s]| where r, s is Real : (G * (1,j)) `1 >= r } = { |[r,s]| where r, s is Real : (G * (1,(1 + 0))) `1 >= r }
;
hence
v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 }
by A5, Def1; verum