let u, v be non zero Element of (TOP-REAL 3); for r being Real st r <> 0 & are_Prop u,v holds
are_Prop r * u,v
let r be Real; ( r <> 0 & are_Prop u,v implies are_Prop r * u,v )
assume that
A1:
r <> 0
and
A2:
are_Prop u,v
; are_Prop r * u,v
consider a being Real such that
A3:
a <> 0
and
A4:
u = a * v
by ANPROJ_1:1, A2;
r * u = (r * a) * v
by A4, RVSUM_1:49;
hence
are_Prop r * u,v
by A1, A3, ANPROJ_1:1; verum