let n be Nat; :: thesis:
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let U be Subspace of n -VectSp_over F_Real; :: thesis:
let W be Subspace of TOP-REAL n; :: thesis:
let LU be Linear_Combination of U; :: thesis:
let LW be Linear_Combination of W; :: thesis:
assume A1: LU = LW ; :: thesis:
reconsider LW9 = LW as Function of the carrier of W,REAL ;
defpred S₁[ 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 & S₁[x,y] )

let x be object ; :: thesis:
assume x in the carrier of (TOP-REAL n) ; :: thesis:
then reconsider x = x as VECTOR of (TOP-REAL n) ;

then reconsider x = x as VECTOR of W ;
S₁[x,LW . x] by A4;
hence ex y being object st
( y in REAL & S₁[x,y] ) ; :: thesis:

end;

end;

let v be VECTOR of (TOP-REAL n); :: thesis:
assume not v in C ; :: thesis:
then ( ( S₁[v,LW . v] & not v in C & v in the carrier of W ) or S₁[v, 0 ] ) by STRUCT_0:def 5;
then ( ( S₁[v,LW . v] & LW . v = 0 ) or S₁[v, 0 ] ) by RLVECT_2:19;
hence L . v = 0 by A5; :: thesis:

end;

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;

end;

end;