let u, v be non zero Element of (TOP-REAL 3); :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: 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 ) ; :: thesis: contradiction

per cases then ( a = 0 or b = 0 ) ;

suppose A6: a = 0 ; :: thesis: contradiction

u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A7: 0 * u = 0* n by EUCLID_4:3;
bv in TOP-REAL 3 ;
then bv in REAL 3 by EUCLID:22;
then (0* n) + bv = bv by EUCLID_4:1;
hence contradiction by A1, A6, A2, A7, Th56; :: thesis: verum

end;

suppose A8: b = 0 ; :: thesis: contradiction

v in TOP-REAL 3 ;
then v in REAL 3 by EUCLID:22;
then A9: 0 * v = 0* n by EUCLID_4:3;
au in TOP-REAL 3 ;
then au in REAL 3 by EUCLID:22;
then au + (0* n) = au by EUCLID_4:1;
hence contradiction by A1, A8, A2, A9, Th56; :: thesis: verum

end;

end;

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