let n be Nat; for U being Subspace of n -VectSp_over F_Real
for W being Subspace of TOP-REAL n
for LU being Linear_Combination of U
for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let U be Subspace of n -VectSp_over F_Real; for W being Subspace of TOP-REAL n
for LU being Linear_Combination of U
for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
let W be Subspace of TOP-REAL n; for LU being Linear_Combination of U
for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
let LU be Linear_Combination of U; for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
let LW be Linear_Combination of W; ( LU = LW implies ( Carrier LU = Carrier LW & Sum LU = Sum LW ) )
assume A1:
LU = LW
; ( Carrier LU = Carrier LW & Sum LU = Sum LW )
reconsider LW9 = LW as Function of the carrier of W,REAL ;
defpred S1[ object , object ] means ( ( $1 in W & $2 = LW . $1 ) or ( not $1 in W & $2 = In (0,REAL) ) );
A2:
( dom LU = [#] U & dom LW = [#] W )
by FUNCT_2:def 1;
A3:
for x being object st x in the carrier of (TOP-REAL n) holds
ex y being object st
( y in REAL & S1[x,y] )
consider L being Function of the carrier of (TOP-REAL n),REAL such that
A5:
for x being object st x in the carrier of (TOP-REAL n) holds
S1[x,L . x]
from FUNCT_2:sch 1(A3);
A6:
the carrier of W c= the carrier of (TOP-REAL n)
by RLSUB_1:def 2;
then reconsider C = Carrier LW as finite Subset of (TOP-REAL n) by XBOOLE_1:1;
A7:
L is Element of Funcs ( the carrier of (TOP-REAL n),REAL)
by FUNCT_2:8;
then reconsider L = L as Linear_Combination of TOP-REAL n by A7, RLVECT_2:def 3;
reconsider L9 = L | the carrier of W as Function of the carrier of W,REAL by A6, FUNCT_2:32;
then A9:
LW = L9
by FUNCT_2:12;
reconsider K = L as Linear_Combination of n -VectSp_over F_Real by Th1;
then A14:
Carrier L c= the carrier of W
;
then A15:
( Carrier L = Carrier LW & Sum L = Sum LW )
by A9, RLVECT_5:10;
A16:
Carrier L = Carrier K
by Th2;
then
Sum K = Sum LU
by A1, A2, A14, A9, VECTSP_9:7;
hence
( Carrier LU = Carrier LW & Sum LU = Sum LW )
by A1, A2, A9, A15, A16, Th5, VECTSP_9:7; verum