let u, v be non zero Element of (TOP-REAL 3); for a, b being Real st ( a <> 0 or b <> 0 ) & (a * u) + (b * v) = 0. (TOP-REAL 3) holds
are_Prop u,v
let a, b be Real; ( ( a <> 0 or b <> 0 ) & (a * u) + (b * v) = 0. (TOP-REAL 3) implies are_Prop u,v )
assume that
A1:
( a <> 0 or b <> 0 )
and
A2:
(a * u) + (b * v) = 0. (TOP-REAL 3)
; are_Prop u,v
reconsider n = 3 as Nat ;
reconsider au = a * u, bv = b * v as Element of (TOP-REAL 3) ;
consider c being Real such that
A3:
c <> 0
and
A4:
au = c * bv
by A2, ANPROJ_1:1, ANPROJ_1:13;
A5:
( a <> 0 & b <> 0 )
proof
assume
(
a = 0 or
b = 0 )
;
contradiction
end;
u =
1 * u
by RVSUM_1:52
.=
((1 / a) * a) * u
by A5, XCMPLX_1:106
.=
(1 / a) * (c * (b * v))
by A4, RVSUM_1:49
.=
((1 / a) * c) * (b * v)
by RVSUM_1:49
.=
(((1 / a) * c) * b) * v
by RVSUM_1:49
;
hence
are_Prop u,v
by A3, A5, ANPROJ_1:1; verum