set Tm = TOP-REAL m;
set Tn = TOP-REAL n;
A1:
now ( n <> 0 implies ex F being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds F . f = Line (((LineVec2Mx (@ f)) * M),1) )assume A2:
n <> 0
;
ex F being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds F . f = Line (((LineVec2Mx (@ f)) * M),1)defpred S1[
Element of
(TOP-REAL n),
Element of
(TOP-REAL m)]
means $2
= Line (
((LineVec2Mx (@ $1)) * M),1);
A3:
for
x being
Element of
(TOP-REAL n) ex
y being
Element of
(TOP-REAL m) st
S1[
x,
y]
consider F being
Function of
(TOP-REAL n),
(TOP-REAL m) such that A5:
for
x being
Element of
(TOP-REAL n) holds
S1[
x,
F . x]
from FUNCT_2:sch 3(A3);
take F =
F;
for f being n -element real-valued FinSequence holds F . f = Line (((LineVec2Mx (@ f)) * M),1)let f be
n -element real-valued FinSequence;
F . f = Line (((LineVec2Mx (@ f)) * M),1)
(
@ f is
FinSequence of
REAL &
len f = n )
by CARD_1:def 7;
then
f is
Element of
n -tuples_on REAL
by FINSEQ_2:92;
then
f in REAL n
;
then
f is
Element of
(TOP-REAL n)
by EUCLID:22;
hence
F . f = Line (
((LineVec2Mx (@ f)) * M),1)
by A5;
verum end;
hence
( ( n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( not n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = 0. (TOP-REAL m) ) )
by A1; verum