let G be X_equal-in-line Matrix of (TOP-REAL 2); :: thesis: card (proj1 .: (Values G)) <= len G
deffunc H₁( Nat) -> Element of REAL = proj1 . (G * $1,1);
consider f being FinSequence such that
A1: len f = len 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 = dom G by A1, FINSEQ_3:31;
proj1 .: (Values G) c= rng f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in proj1 .: (Values G) or y in rng f )
A4: Values G = { (G * i,j) where i, j is Element of NAT : [i,j] in Indices G } by GOBRD13:7;
assume y in proj1 .: (Values G) ; :: thesis: y in rng f
then consider x being set such that
A5: x in the carrier of (TOP-REAL 2) and
A6: x in Values G and
A7: y = proj1 . x by FUNCT_2:115;
consider i, j being Element of 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 <= j & j <= width G ) by A9, MATRIX_1:39;
A11: ( 1 <= i & i <= len G ) by A9, MATRIX_1:39;
then A12: i in dom G by FINSEQ_3:27;
y = x `1 by A7, PSCOMP_1:def 28
.= (G * i,1) `1 by A8, A11, A10, GOBOARD5:3
.= proj1 . (G * i,1) by PSCOMP_1:def 28
.= f . i by A2, A3, A12 ;
hence y in rng f by A3, A12, FUNCT_1:12; :: thesis: verum

end;

then card (proj1 .: (Values G)) c= card (dom G) by A3, CARD_1:28;
then card (proj1 .: (Values G)) <= card (dom G) by NAT_1:40;
hence card (proj1 .: (Values G)) <= len G by CARD_1:104; :: thesis: verum