let V be RealLinearSpace; :: thesis: for u, v being Element of V st ( for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) holds

( not u is zero & not v is zero & not are_Prop u,v )

let u, v be Element of V; :: thesis: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) implies ( not u is zero & not v is zero & not are_Prop u,v ) )

assume A1: for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ; :: thesis: ( not u is zero & not v is zero & not are_Prop u,v )

given a, b being Real such that A5: a * u = b * v and

A6: a <> 0 and

b <> 0 ; :: according to ANPROJ_1:def 1 :: thesis: contradiction

0. V = (a * u) - (b * v) by A5, RLVECT_1:15

.= (a * u) + (b * (- v)) by RLVECT_1:25

.= (a * u) + ((- b) * v) by RLVECT_1:24 ;

hence contradiction by A1, A6; :: thesis: verum

( a = 0 & b = 0 ) ) holds

( not u is zero & not v is zero & not are_Prop u,v )

let u, v be Element of V; :: thesis: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) implies ( not u is zero & not v is zero & not are_Prop u,v ) )

assume A1: for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ; :: thesis: ( not u is zero & not v is zero & not are_Prop u,v )

A2: now :: thesis: not v is zero

assume
v is zero
; :: thesis: contradiction

then A3: v = 0. V ;

0. V = (0. V) + (0. V) by RLVECT_1:4

.= (0. V) + (1 * v) by A3, RLVECT_1:def 8

.= (0 * u) + (1 * v) by RLVECT_1:10 ;

hence contradiction by A1; :: thesis: verum

end;then A3: v = 0. V ;

0. V = (0. V) + (0. V) by RLVECT_1:4

.= (0. V) + (1 * v) by A3, RLVECT_1:def 8

.= (0 * u) + (1 * v) by RLVECT_1:10 ;

hence contradiction by A1; :: thesis: verum

now :: thesis: not u is zero

hence
( not u is zero & not v is zero )
by A2; :: thesis: not are_Prop u,vassume
u is zero
; :: thesis: contradiction

then A4: u = 0. V ;

0. V = (0. V) + (0. V) by RLVECT_1:4

.= (1 * u) + (0. V) by A4, RLVECT_1:def 8

.= (1 * u) + (0 * v) by RLVECT_1:10 ;

hence contradiction by A1; :: thesis: verum

end;then A4: u = 0. V ;

0. V = (0. V) + (0. V) by RLVECT_1:4

.= (1 * u) + (0. V) by A4, RLVECT_1:def 8

.= (1 * u) + (0 * v) by RLVECT_1:10 ;

hence contradiction by A1; :: thesis: verum

given a, b being Real such that A5: a * u = b * v and

A6: a <> 0 and

b <> 0 ; :: according to ANPROJ_1:def 1 :: thesis: contradiction

0. V = (a * u) - (b * v) by A5, RLVECT_1:15

.= (a * u) + (b * (- v)) by RLVECT_1:25

.= (a * u) + ((- b) * v) by RLVECT_1:24 ;

hence contradiction by A1, A6; :: thesis: verum