let n be Nat; :: thesis: for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Carrier Lr = Carrier Lv
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let Lv be Linear_Combination of n -VectSp_over F_Real; :: thesis: for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Carrier Lr = Carrier Lv
let Lr be Linear_Combination of TOP-REAL n; :: thesis: ( Lr = Lv implies Carrier Lr = Carrier Lv )
assume A1: Lr = Lv ; :: thesis: Carrier Lr = Carrier Lv
thus Carrier Lr c= Carrier Lv :: according to XBOOLE_0:def 10 :: thesis: Carrier Lv c= Carrier Lr
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier Lr or x in Carrier Lv )
assume A2: x in Carrier Lr ; :: thesis: x in Carrier Lv
then reconsider v = x as Element of (TOP-REAL n) ;
reconsider u = v as Element of (n -VectSp_over F_Real) by Lm1;
Lv . u <> 0. F_Real by A1, A2, RLVECT_2:19;
hence x in Carrier Lv by VECTSP_6:1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier Lv or x in Carrier Lr )
assume x in Carrier Lv ; :: thesis: x in Carrier Lr
then consider u being Element of (n -VectSp_over F_Real) such that
A3: x = u and
A4: Lv . u <> 0. F_Real by VECTSP_6:1;
reconsider v = u as Element of (TOP-REAL n) by Lm1;
v in Carrier Lr by A1, A4, RLVECT_2:19;
hence x in Carrier Lr by A3; :: thesis: verum