set Tm = TOP-REAL m;
set Tn = TOP-REAL n;

A1: now :: thesis: ( 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 ; :: thesis: 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 S₁[ 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 S₁[x,y]

proof

let x be Element of (TOP-REAL n); :: thesis: ex y being Element of (TOP-REAL m) st S₁[x,y]
set L = LineVec2Mx (@ x);
set LL = Line (((LineVec2Mx (@ x)) * M),1);
len x = n by CARD_1:def 7;
then A4: width (LineVec2Mx (@ x)) = n by MATRIX13:1;
( len M = n & width M = m ) by A2, MATRIX13:1;
then width ((LineVec2Mx (@ x)) * M) = m by A4, MATRIX_3:def 4;
then Line (((LineVec2Mx (@ x)) * M),1) in REAL m ;
then reconsider LL = Line (((LineVec2Mx (@ x)) * M),1) as Element of (TOP-REAL m) by EUCLID:22;
S₁[x,LL] ;
hence ex y being Element of (TOP-REAL m) st S₁[x,y] ; :: thesis: verum

end;

consider F being Function of (TOP-REAL n),(TOP-REAL m) such that
A5: for x being Element of (TOP-REAL n) holds S₁[x,F . x] from FUNCT_2:sch 3(A3);
take F = F; :: thesis: for f being n -element real-valued FinSequence holds F . f = Line (((LineVec2Mx (@ f)) * M),1)
let f be n -element real-valued FinSequence; :: thesis: 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; :: thesis: verum

end;

now :: thesis: ( 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 = 0. (TOP-REAL m) )

assume n = 0 ; :: thesis: ex F being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds F . f = 0. (TOP-REAL m)
defpred S₁[ Element of (TOP-REAL n), Element of (TOP-REAL m)] means $2 = 0. (TOP-REAL m);
A6: for x being Element of (TOP-REAL n) ex y being Element of (TOP-REAL m) st S₁[x,y] ;
consider F being Function of (TOP-REAL n),(TOP-REAL m) such that
A7: for x being Element of (TOP-REAL n) holds S₁[x,F . x] from FUNCT_2:sch 3(A6);
take F = F; :: thesis: for f being n -element real-valued FinSequence holds F . f = 0. (TOP-REAL m)
let f be n -element real-valued FinSequence; :: thesis: F . f = 0. (TOP-REAL m)
( @ 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 = 0. (TOP-REAL m) by A7; :: thesis: verum

end;

hence ( ( n <> 0 implies ex b₁ being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b₁ . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( not n <> 0 implies ex b₁ being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b₁ . f = 0. (TOP-REAL m) ) ) by A1; :: thesis: verum