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 )

( 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

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 :: thesis: ( not are_Prop u,v & u is zero implies 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 ) )

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

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;

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, Th3, Th10;

( 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, Th3, Th10;

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, Th2; :: thesis: verum

end;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;

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, Th3, Th10;

( 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, Th3, Th10;

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, Th2; :: thesis: verum

A8: now :: thesis: ( not are_Prop u,v & not u is zero & not v is zero implies ( not u + v is zero & u,v,u + v are_LinDep & not are_Prop u,u + v & not are_Prop v,u + v ) )

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, Th13;

hence not u + v is zero ; :: 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)

.= 0. V by RLVECT_1:5 ;

hence u,v,u + v are_LinDep ; :: thesis: ( not are_Prop u,u + v & not are_Prop v,u + v )

A12: v <> 0. V by A11;

A14: u <> 0. V by A10;

end;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, Th13;

hence not u + v is zero ; :: 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)

.= 0. V by RLVECT_1:5 ;

hence u,v,u + v are_LinDep ; :: thesis: ( not are_Prop u,u + v & not are_Prop v,u + v )

A12: v <> 0. V by A11;

now :: thesis: for a, b being Real holds

( not a * u = b * (u + v) or a = 0 or b = 0 )

hence
not are_Prop u,u + v
; :: thesis: not are_Prop v,u + v( not a * u = b * (u + v) or a = 0 or b = 0 )

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 ;

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 ;

end;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 ;

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 :: thesis: ( a + (- b) = 0 implies b = 0 )

hence
( a = 0 or b = 0 )
by A9, A13; :: thesis: verumassume
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;then b * v = 0. V by A13, RLVECT_1:10;

hence b = 0 by A12, RLVECT_1:11; :: thesis: verum

A14: u <> 0. V by A10;

now :: thesis: for a, b being Real holds

( not a * v = b * (u + v) or a = 0 or b = 0 )

hence
not are_Prop v,u + v
; :: thesis: verum( not a * v = b * (u + v) or a = 0 or b = 0 )

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 ;

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 ;

end;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 ;

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 :: thesis: ( a + (- b) = 0 implies b = 0 )

hence
( a = 0 or b = 0 )
by A9, A15; :: thesis: verumassume
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;then b * u = 0. V by A15, RLVECT_1:10;

hence b = 0 by A14, RLVECT_1:11; :: thesis: verum

A16: now :: thesis: ( not are_Prop u,v & v is zero implies 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 ) )

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

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;

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, Th3, Th10;

( 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, Th3, Th10;

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, Th2; :: thesis: verum

end;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;

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, Th3, Th10;

( 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, Th3, Th10;

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, Th2; :: thesis: verum

now :: thesis: ( are_Prop u,v implies 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 ) )

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 ) )

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, Th2, Th11;

( 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, Th2, Th11;

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, Th2; :: thesis: verum

end;( 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, Th2, Th11;

( 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, Th2, Th11;

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, Th2; :: thesis: verum

( 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