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

( a = 0 & b = 0 & c = 0 ) ) holds

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

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

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

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

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

thus not u,v,w are_LinDep by A1; :: thesis: not are_Prop u,v

hence not are_Prop u,v by ANPROJ_1:12; :: thesis: verum

( a = 0 & b = 0 & c = 0 ) ) holds

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

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

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

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

( a = 0 & b = 0 & c = 0 ) ; :: thesis: ( not u is zero & not v is zero & not w is zero & not u,v,w are_LinDep & 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) + (0. V)) + (0. V) by RLVECT_1:4

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

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

.= ((0 * u) + (1 * v)) + (0 * w) 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) + (0. V)) + (0. V) by RLVECT_1:4

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

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

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

hence contradiction by A1; :: thesis: verum

A4: now :: thesis: not w is zero

assume
w is zero
; :: thesis: contradiction

then A5: w = 0. V ;

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

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

.= ((0. V) + (0. V)) + (1 * w) by A5, RLVECT_1:def 8

.= ((0 * u) + (0. V)) + (1 * w) by RLVECT_1:10

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

hence contradiction by A1; :: thesis: verum

end;then A5: w = 0. V ;

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

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

.= ((0. V) + (0. V)) + (1 * w) by A5, RLVECT_1:def 8

.= ((0 * u) + (0. V)) + (1 * w) by RLVECT_1:10

.= ((0 * u) + (0 * v)) + (1 * w) 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 & not w is zero )
by A2, A4; :: thesis: ( not u,v,w are_LinDep & not are_Prop u,v )assume
u is zero
; :: thesis: contradiction

then A6: u = 0. V ;

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

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

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

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

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

hence contradiction by A1; :: thesis: verum

end;then A6: u = 0. V ;

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

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

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

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

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

hence contradiction by A1; :: thesis: verum

thus not u,v,w are_LinDep by A1; :: thesis: not are_Prop u,v

hence not are_Prop u,v by ANPROJ_1:12; :: thesis: verum