let G be X_equal-in-line Matrix of (TOP-REAL 2); card (proj1 .: (Values G)) <= len G
deffunc H1( Nat) -> set = 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 = H1(k)
from FINSEQ_1:sch 2();
A3:
dom f = dom G
by A1, FINSEQ_3:29;
proj1 .: (Values G) c= rng f
proof
let y be
object ;
TARSKI:def 3 ( not y in proj1 .: (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 proj1 .: (Values G)
;
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 = proj1 . 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
<= j &
j <= width G )
by A9, MATRIX_0:32;
A11:
( 1
<= i &
i <= len G )
by A9, MATRIX_0:32;
then A12:
i in dom G
by FINSEQ_3:25;
y =
x `1
by A7, PSCOMP_1:def 5
.=
(G * (i,1)) `1
by A8, A11, A10, GOBOARD5:2
.=
proj1 . (G * (i,1))
by PSCOMP_1:def 5
.=
f . i
by A2, A3, A12
;
hence
y in rng f
by A3, A12, FUNCT_1:3;
verum
end;
then
Segm (card (proj1 .: (Values G))) c= Segm (card (dom G))
by A3, CARD_1:12;
then
card (proj1 .: (Values G)) <= card (dom G)
by NAT_1:39;
hence
card (proj1 .: (Values G)) <= len G
by CARD_1:62; verum