let G be V9() Y_equal-in-column Matrix of (TOP-REAL 2); :: thesis: card (proj2 .: (Values G)) <= width G
deffunc H1( Nat) -> Element of REAL = 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 = H1(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
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in proj2 .: (Values G) or y in rng f )
assume
y in proj2 .: (Values G)
;
:: thesis: y in rng f
then consider x being
set such that A4:
x in the
carrier of
(TOP-REAL 2)
and A5:
x in Values G
and A6:
y = proj2 . x
by FUNCT_2:115;
Values G = { (G * i,j) where i, j is Element of NAT : [i,j] in Indices G }
by GOBRD13:7;
then consider i,
j being
Element of
NAT such that A7:
x = G * i,
j
and A8:
[i,j] in Indices G
by A5;
A9:
( 1
<= j &
j <= width G )
by A8, MATRIX_1:39;
then A10:
j in Seg (width G)
by FINSEQ_1:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A4;
A11:
( 1
<= i &
i <= len G )
by A8, MATRIX_1:39;
y =
x `2
by A6, PSCOMP_1:def 29
.=
(G * 1,j) `2
by A7, A9, A11, GOBOARD5:2
.=
proj2 . (G * 1,j)
by PSCOMP_1:def 29
.=
f . j
by A2, A10, A3
;
hence
y in rng f
by A3, A10, FUNCT_1:12;
:: thesis: verum
end;
then
card (proj2 .: (Values G)) c= card (Seg (width G))
by A3, CARD_1:28;
then
card (proj2 .: (Values G)) <= card (Seg (width G))
by NAT_1:40;
hence
card (proj2 .: (Values G)) <= width G
by FINSEQ_1:78; :: thesis: verum