let V be RealLinearSpace; for u, v, u1, v1 being Element of V st ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) holds
for y being Element of V holds
( y is zero or not u,v,y are_LinDep or not u1,v1,y are_LinDep )
let u, v, u1, v1 be Element of V; ( ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) implies for y being Element of V holds
( y is zero or not u,v,y are_LinDep or not u1,v1,y are_LinDep ) )
assume A1:
for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 )
; for y being Element of V holds
( y is zero or not u,v,y are_LinDep or not u1,v1,y are_LinDep )
then A2:
not are_Prop u,v
by Th2;
assume
ex y being Element of V st
( not y is zero & u,v,y are_LinDep & u1,v1,y are_LinDep )
; contradiction
then consider y being Element of V such that
A3:
not y is zero
and
A4:
u,v,y are_LinDep
and
A5:
u1,v1,y are_LinDep
;
( not u is zero & not v is zero )
by A1, Th2;
then consider a, b being Real such that
A6:
y = (a * u) + (b * v)
by A4, A2, ANPROJ_1:6;
A7:
not are_Prop u1,v1
by A1, Th2;
( not u1 is zero & not v1 is zero )
by A1, Th2;
then consider a1, b1 being Real such that
A8:
y = (a1 * u1) + (b1 * v1)
by A5, A7, ANPROJ_1:6;
0. V =
((a * u) + (b * v)) - ((a1 * u1) + (b1 * v1))
by A6, A8, RLVECT_1:15
.=
((a * u) + (b * v)) + ((- 1) * ((a1 * u1) + (b1 * v1)))
by RLVECT_1:16
.=
((a * u) + (b * v)) + (((- 1) * (a1 * u1)) + ((- 1) * (b1 * v1)))
by RLVECT_1:def 5
.=
((a * u) + (b * v)) + ((((- 1) * a1) * u1) + ((- 1) * (b1 * v1)))
by RLVECT_1:def 7
.=
((a * u) + (b * v)) + ((((- 1) * a1) * u1) + (((- 1) * b1) * v1))
by RLVECT_1:def 7
.=
(((a * u) + (b * v)) + (((- 1) * a1) * u1)) + (((- 1) * b1) * v1)
by RLVECT_1:def 3
;
then
( a = 0 & b = 0 )
by A1;
then y =
(0. V) + (0 * v)
by A6, RLVECT_1:10
.=
(0. V) + (0. V)
by RLVECT_1:10
.=
0. V
by RLVECT_1:4
;
hence
contradiction
by A3; verum