let V be RealLinearSpace; :: thesis: for p, q being Element of V st not are_Prop p,q & not p is zero & not q is zero holds
for u, v being Element of V ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
let p, q be Element of V; :: thesis: ( not are_Prop p,q & not p is zero & not q is zero implies for u, v being Element of V ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) )
assume that
A1: not are_Prop p,q and
A2: not p is zero and
A3: not q is zero ; :: thesis: for u, v being Element of V ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
let u, v be Element of V; :: thesis: ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )

A6: now

assume that
not are_Prop u,v and
A7: u is zero ; :: thesis: ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
A8: u = 0. V by A7, STRUCT_0:def 12;
then A9: ( not are_Prop v,q implies ( not are_Prop v,q & not q is zero & u,v,q are_LinDep & not are_Prop u,q ) ) by A3, Th7, Th15;
( not are_Prop v,p implies ( not are_Prop v,p & not p is zero & u,v,p are_LinDep & not are_Prop u,p ) ) by A2, A8, Th7, Th15;
hence ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) by A1, A9, Th6; :: thesis: verum

end;

A10: now

set y = u + v;
assume that
A11: not are_Prop u,v and
A12: not u is zero and
A13: not v is zero ; :: thesis: ( not u + v is zero & u,v,u + v are_LinDep & not are_Prop u,u + v & not are_Prop v,u + v )
u + v <> 0. V by A11, Th18;
hence not u + v is zero by STRUCT_0:def 12; :: thesis: ( u,v,u + v are_LinDep & not are_Prop u,u + v & not are_Prop v,u + v )
((1 * u) + (1 * v)) + ((- 1) * (u + v)) = (u + (1 * v)) + ((- 1) * (u + v)) by RLVECT_1:def 11
.= (u + v) + ((- 1) * (u + v)) by RLVECT_1:def 11
.= (u + v) + (- (u + v)) by RLVECT_1:29
.= (v + u) + ((- u) + (- v)) by RLVECT_1:45
.= v + (u + ((- u) + (- v))) by RLVECT_1:def 6
.= v + ((u + (- u)) + (- v)) by RLVECT_1:def 6
.= v + ((0. V) + (- v)) by RLVECT_1:16
.= v + (- v) by RLVECT_1:10
.= 0. V by RLVECT_1:16 ;
hence u,v,u + v are_LinDep by Def3; :: thesis: ( not are_Prop u,u + v & not are_Prop v,u + v )
A14: v <> 0. V by A13;

now

let a, b be Real; :: thesis: ( not a * u = b * (u + v) or a = 0 or b = 0 )
assume a * u = b * (u + v) ; :: thesis: ( a = 0 or b = 0 )
then (- (b * u)) + (a * u) = (- (b * u)) + ((b * u) + (b * v)) by RLVECT_1:def 8
.= ((b * u) + (- (b * u))) + (b * v) by RLVECT_1:def 6
.= (0. V) + (b * v) by RLVECT_1:16
.= b * v by RLVECT_1:10 ;
then A15: b * v = (a * u) + (b * (- u)) by RLVECT_1:39
.= (a * u) + ((- b) * u) by RLVECT_1:38
.= (a + (- b)) * u by RLVECT_1:def 9 ;

now

assume a + (- b) = 0 ; :: thesis: b = 0
then b * v = 0. V by A15, RLVECT_1:23;
hence b = 0 by A14, RLVECT_1:24; :: thesis: verum

end;

hence ( a = 0 or b = 0 ) by A11, A15, Def2; :: thesis: verum

end;

hence not are_Prop u,u + v by Def2; :: thesis: not are_Prop v,u + v
A16: u <> 0. V by A12;

now

let a, b be Real; :: thesis: ( not a * v = b * (u + v) or a = 0 or b = 0 )
assume a * v = b * (u + v) ; :: thesis: ( a = 0 or b = 0 )
then (a * v) + (- (b * v)) = ((b * u) + (b * v)) + (- (b * v)) by RLVECT_1:def 8
.= (b * u) + ((b * v) + (- (b * v))) by RLVECT_1:def 6
.= (b * u) + (0. V) by RLVECT_1:16
.= b * u by RLVECT_1:10 ;
then A17: b * u = (a * v) + (b * (- v)) by RLVECT_1:39
.= (a * v) + ((- b) * v) by RLVECT_1:38
.= (a + (- b)) * v by RLVECT_1:def 9 ;

now

assume a + (- b) = 0 ; :: thesis: b = 0
then b * u = 0. V by A17, RLVECT_1:23;
hence b = 0 by A16, RLVECT_1:24; :: thesis: verum

end;

hence ( a = 0 or b = 0 ) by A11, A17, Def2; :: thesis: verum

end;

hence not are_Prop v,u + v by Def2; :: thesis: verum

end;

A18: now

assume that
not are_Prop u,v and
A19: v is zero ; :: thesis: ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
A20: v = 0. V by A19, STRUCT_0:def 12;
then A21: ( not are_Prop u,q implies ( not q is zero & u,v,q are_LinDep & not are_Prop u,q & not are_Prop v,q ) ) by A3, Th7, Th15;
( not are_Prop u,p implies ( not p is zero & u,v,p are_LinDep & not are_Prop u,p & not are_Prop v,p ) ) by A2, A20, Th7, Th15;
hence ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) by A1, A21, Th6; :: thesis: verum

end;

now

assume A22: are_Prop u,v ; :: thesis: ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
then A23: ( not are_Prop u,q implies ( not q is zero & u,v,q are_LinDep & not are_Prop u,q & not are_Prop v,q ) ) by A3, Th6, Th16;
( not are_Prop u,p implies ( not p is zero & u,v,p are_LinDep & not are_Prop u,p & not are_Prop v,p ) ) by A2, A22, Th6, Th16;
hence ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) by A1, A23, Th6; :: thesis: verum

end;

hence ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) by A10, A6, A18; :: thesis: verum