let V be RealLinearSpace; :: thesis: Lin ({} the carrier of V) = (0). V

set A = Lin ({} the carrier of V);

set A = Lin ({} the carrier of V);

now :: thesis: for v being VECTOR of V holds

( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )

hence
Lin ({} the carrier of V) = (0). V
by RLSUB_1:31; :: thesis: verum( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )

let v be VECTOR of V; :: thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )

thus ( v in Lin ({} the carrier of V) implies v in (0). V ) :: thesis: ( v in (0). V implies v in Lin ({} the carrier of V) )

then v = 0. V by Lm2;

hence v in Lin ({} the carrier of V) by RLSUB_1:17; :: thesis: verum

end;thus ( v in Lin ({} the carrier of V) implies v in (0). V ) :: thesis: ( v in (0). V implies v in Lin ({} the carrier of V) )

proof

assume
v in (0). V
; :: thesis: v in Lin ({} the carrier of V)
assume
v in Lin ({} the carrier of V)
; :: thesis: v in (0). V

then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def 5;

the carrier of (Lin ({} the carrier of V)) = { (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum } by Def2;

then ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1;

then v = 0. V by RLVECT_2:31;

hence v in (0). V by Lm2; :: thesis: verum

end;then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def 5;

the carrier of (Lin ({} the carrier of V)) = { (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum } by Def2;

then ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1;

then v = 0. V by RLVECT_2:31;

hence v in (0). V by Lm2; :: thesis: verum

then v = 0. V by Lm2;

hence v in Lin ({} the carrier of V) by RLSUB_1:17; :: thesis: verum