let T be RealLinearSpace; :: thesis: for Lv being Linear_Combination of RLSp2RVSp T
for Lr being Linear_Combination of T st Lr = Lv holds
Carrier Lr = Carrier Lv
let Lv be Linear_Combination of RLSp2RVSp T; :: thesis: for Lr being Linear_Combination of T st Lr = Lv holds
Carrier Lr = Carrier Lv
let Lr be Linear_Combination of T; :: 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 T ;
reconsider u = v as Element of (RLSp2RVSp T) ;
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 (RLSp2RVSp T) such that
A3: x = u and
A4: Lv . u <> 0. F_Real by VECTSP_6:1;
thus x in Carrier Lr by A1, A4, RLVECT_2:19, A3; :: thesis: verum