let G be empty-yielding Y_equal-in-column Matrix of (TOP-REAL 2); :: thesis: card (proj2 .: (Values G)) <= width G
deffunc H₁( Nat) -> set = proj2 . (G * (1,$1));
consider f being FinSequence such that
A1: len f = width G and
A2: for k being Nat st k in dom f holds
f . k = H₁(k) from FINSEQ_1:sch 2();
A3: dom f = Seg (width G) by A1, FINSEQ_1:def 3;
proj2 .: (Values G) c= rng f

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 .: (Values G) or y in rng f )
A4: Values G = { (G * (i,j)) where i, j is Nat : [i,j] in Indices G } by MATRIX_0:39;
assume y in proj2 .: (Values G) ; :: thesis: y in rng f
then consider x being object such that
A5: x in the carrier of (TOP-REAL 2) and
A6: x in Values G and
A7: y = proj2 . x by FUNCT_2:64;
consider i, j being Nat such that
A8: x = G * (i,j) and
A9: [i,j] in Indices G by A6, A4;
reconsider x = x as Point of (TOP-REAL 2) by A5;
A10: ( 1 <= i & i <= len G ) by A9, MATRIX_0:32;
A11: ( 1 <= j & j <= width G ) by A9, MATRIX_0:32;
then A12: j in Seg (width G) by FINSEQ_1:1;
y = x `2 by A7, PSCOMP_1:def 6
.= (G * (1,j)) `2 by A8, A11, A10, GOBOARD5:1
.= proj2 . (G * (1,j)) by PSCOMP_1:def 6
.= f . j by A2, A3, A12 ;
hence y in rng f by A3, A12, FUNCT_1:3; :: thesis: verum

end;

then Segm (card (proj2 .: (Values G))) c= Segm (card (Seg (width G))) by A3, CARD_1:12;
then card (proj2 .: (Values G)) <= card (Seg (width G)) by NAT_1:39;
hence card (proj2 .: (Values G)) <= width G by FINSEQ_1:57; :: thesis: verum