let n be Nat; :: thesis:
let F be one-to-one FinSequence of (TOP-REAL n); :: thesis:
assume A1: rng F is linearly-independent ; :: thesis:
reconsider f = F as FinSequence of (n -VectSp_over F_Real) by Lm1;
set MF = FinS2MX f;
set n1 = n -' (len F);
set L = len F;
lines (FinS2MX f) is linearly-independent by A1, Th7;
then the_rank_of (FinS2MX f) = len F by MATRIX13:121;
then len F <= width (FinS2MX f) by MATRIX13:74;
then A2: len F <= n by MATRIX_0:23;
then A3: n - (len F) = n -' (len F) by XREAL_1:233;
set V = n -VectSp_over F_Real;
let B be OrdBasis of n -VectSp_over F_Real; :: thesis:
assume A4: B = MX2FinS (1. (F_Real,n)) ; :: thesis:
let M be Matrix of n,F_Real; :: thesis:
assume that
M is invertible and
A5: M | (len F) = F ; :: thesis:
consider q being FinSequence such that
A6: M = F ^ q by A5, FINSEQ_1:80;
M = MX2FinS M ;
then reconsider q = q as FinSequence of (n -VectSp_over F_Real) by A6, FINSEQ_1:36;
A7: len M = (len F) + (len q) by A6, FINSEQ_1:22;
set Mq = FinS2MX q;
set MT = Mx2Tran M;
A8: len M = n by MATRIX_0:def 2;
A9: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:52;
A10: dom (Mx2Tran (FinS2MX f)) = [#] (TOP-REAL (len F)) by FUNCT_2:def 1;
A11: the carrier of (TOP-REAL n) = REAL n by EUCLID:22
.= n -tuples_on REAL ;
A12: rng (Mx2Tran (FinS2MX f)) = [#] (Lin (lines (FinS2MX f))) by Th18
.= [#] (Lin (rng F)) by Th6 ;
A13: n |-> 0 = 0* n
.= 0. (TOP-REAL n) by EUCLID:70 ;
A14: (n -' (len F)) |-> 0 = 0* (n -' (len F))
.= 0. (TOP-REAL (n -' (len F))) by EUCLID:70 ;
then A15: (Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0) = 0. (TOP-REAL n) by A3, A8, A7, MATRTOP1:29;
thus (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) c= [#] (Lin (rng F)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) ; :: thesis:
then consider x being object such that
A16: x in dom (Mx2Tran M) and
A17: x in [#] (Lin (rng (B | (len F)))) and
A18: (Mx2Tran M) . x = y by FUNCT_1:def 6;
reconsider x = x as Element of (TOP-REAL n) by A16;
len x = n by CARD_1:def 7;
then len (x | (len F)) = len F by A2, FINSEQ_1:59;
then A19: x | (len F) is len F -element by CARD_1:def 7;
then A20: x | (len F) is Element of (TOP-REAL (len F)) by Lm3;
A21: (Mx2Tran (FinS2MX f)) . (x | (len F)) is Element of n -tuples_on REAL by A11, A19, Lm3;
x in Lin (rng (B | (len F))) by A17;
then x = (x | (len F)) ^ ((n -' (len F)) |-> 0) by A4, Th20;
then y = ((Mx2Tran (FinS2MX f)) . (x | (len F))) + ((Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0)) by A3, A8, A6, A7, A18, A19, MATRTOP1:36
.= (Mx2Tran (FinS2MX f)) . (x | (len F)) by A13, A15, A21, RVSUM_1:16 ;
hence y in [#] (Lin (rng F)) by A12, A10, A20, FUNCT_1:def 3; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in [#] (Lin (rng F)) ; :: thesis:
then consider x being object such that
A22: x in dom (Mx2Tran (FinS2MX f)) and
A23: (Mx2Tran (FinS2MX f)) . x = y by A12, FUNCT_1:def 3;
reconsider x = x as Element of (TOP-REAL (len F)) by A22;
(Mx2Tran (FinS2MX f)) . x is Element of (TOP-REAL n) by Lm3;
then A24: y = ((Mx2Tran (FinS2MX f)) . x) + (0. (TOP-REAL n)) by A11, A13, A23, RVSUM_1:16
.= ((Mx2Tran (FinS2MX f)) . x) + ((Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0)) by A3, A8, A7, A14, MATRTOP1:29
.= (Mx2Tran M) . (x ^ ((n -' (len F)) |-> 0)) by A6, A3, A8, A7, MATRTOP1:36 ;
set xx = x ^ ((n -' (len F)) |-> 0);
len x = len F by CARD_1:def 7;
then dom x = Seg (len F) by FINSEQ_1:def 3;
then x ^ ((n -' (len F)) |-> 0) = ((x ^ ((n -' (len F)) |-> 0)) | (len F)) ^ ((n -' (len F)) |-> 0) by FINSEQ_1:21;
then x ^ ((n -' (len F)) |-> 0) in Lin (rng (B | (len F))) by A4, A3, Th20;
then A25: x ^ ((n -' (len F)) |-> 0) in [#] (Lin (rng (B | (len F)))) ;
x ^ ((n -' (len F)) |-> 0) is Element of (TOP-REAL n) by A3, Lm3;
hence y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) by A9, A24, A25, FUNCT_1:def 6; :: thesis: