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 A1: ( not are_Prop p,q & not p is zero & 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 )
then A2: ( p <> 0. V & q <> 0. V ) by STRUCT_0:def 15;
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 )

A3: now

assume A4: ( not are_Prop u,v & not u is zero & 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 )
then A5: u + v <> 0. V by Th18;
set y = u + v;
A6: ( u <> 0. V & v <> 0. V ) by A4, STRUCT_0:def 15;
thus not u + v is zero by A5, STRUCT_0:def 15; :: 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 9
.= (u + v) + ((- 1) * (u + v)) by RLVECT_1:def 9
.= (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 )

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 9
.= ((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 A7: 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 A7, RLVECT_1:23;
hence b = 0 by A6, RLVECT_1:24; :: thesis: verum

end;

hence ( a = 0 or b = 0 ) by A4, A7, Def2; :: thesis: verum

end;

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

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 9
.= (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 A8: 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 A8, RLVECT_1:23;
hence b = 0 by A6, RLVECT_1:24; :: thesis: verum

end;

hence ( a = 0 or b = 0 ) by A4, A8, Def2; :: thesis: verum

end;

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

end;

A9: now

assume A10: 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 A11: ( 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 A1, Th6, Th16;
( 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 A1, A10, 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, A11, Th6; :: thesis: verum

end;

A12: now

assume ( not are_Prop u,v & 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 )
then A13: u = 0. V by STRUCT_0:def 15;
then A14: ( 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 A1, A2, Th7, Th15;
( 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 A1, A2, A13, 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, A14, Th6; :: thesis: verum

end;

now

assume ( not are_Prop u,v & 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 )
then A15: v = 0. V by STRUCT_0:def 15;
then A16: ( 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 A1, A2, Th7, Th15;
( 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 A1, A2, A15, 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, A16, 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 A3, A9, A12; :: thesis: verum