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 )

A4: now

assume that
not are_Prop u,v and
A5: 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 )
A6: u = 0. V by A5, STRUCT_0:def 12;
then A7: ( 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, A6, 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, A7, Th6; :: thesis: verum

end;

A8: now

set y = u + v;
assume that
A9: not are_Prop u,v and
A10: not u is zero and
A11: 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 A9, 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 8
.= (u + v) + ((- 1) * (u + v)) by RLVECT_1:def 8
.= (u + v) + (- (u + v)) by RLVECT_1:16
.= (v + u) + ((- u) + (- v)) by RLVECT_1:31
.= v + (u + ((- u) + (- v))) by RLVECT_1:def 3
.= v + ((u + (- u)) + (- v)) by RLVECT_1:def 3
.= v + ((0. V) + (- v)) by RLVECT_1:5
.= v + (- v) by RLVECT_1:4
.= 0. V by RLVECT_1:5 ;
hence u,v,u + v are_LinDep by Def3; :: thesis: ( not are_Prop u,u + v & not are_Prop v,u + v )
A12: v <> 0. V by A11;

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 5
.= ((b * u) + (- (b * u))) + (b * v) by RLVECT_1:def 3
.= (0. V) + (b * v) by RLVECT_1:5
.= b * v by RLVECT_1:4 ;
then A13: b * v = (a * u) + (b * (- u)) by RLVECT_1:25
.= (a * u) + ((- b) * u) by RLVECT_1:24
.= (a + (- b)) * u by RLVECT_1:def 6 ;

now

assume a + (- b) = 0 ; :: thesis: b = 0
then b * v = 0. V by A13, RLVECT_1:10;
hence b = 0 by A12, RLVECT_1:11; :: thesis: verum

end;

hence ( a = 0 or b = 0 ) by A9, A13, Def2; :: thesis: verum

end;

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

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 5
.= (b * u) + ((b * v) + (- (b * v))) by RLVECT_1:def 3
.= (b * u) + (0. V) by RLVECT_1:5
.= b * u by RLVECT_1:4 ;
then A15: b * u = (a * v) + (b * (- v)) by RLVECT_1:25
.= (a * v) + ((- b) * v) by RLVECT_1:24
.= (a + (- b)) * v by RLVECT_1:def 6 ;

now

assume a + (- b) = 0 ; :: thesis: b = 0
then b * u = 0. V by A15, RLVECT_1:10;
hence b = 0 by A14, RLVECT_1:11; :: thesis: verum

end;

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

end;

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

end;

A16: now

assume that
not are_Prop u,v and
A17: 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 )
A18: v = 0. V by A17, STRUCT_0:def 12;
then A19: ( 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, A18, 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, A19, Th6; :: thesis: verum

end;

now

assume A20: 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 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, 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, A20, 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, A21, 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 A8, A4, A16; :: thesis: verum