let n be Nat; :: thesis: for x1, x2 being Element of REAL n st x1 // x2 holds
ex a being Real st
( a <> 0 & x1 = a * x2 )
let x1, x2 be Element of REAL n; :: thesis: ( x1 // x2 implies ex a being Real st
( a <> 0 & x1 = a * x2 ) )
assume A1: x1 // x2 ; :: thesis: ex a being Real st
( a <> 0 & x1 = a * x2 )
then consider a being Real such that
A2: x1 = a * x2 ;
x1 <> 0* n by A1;
then a <> 0 by A2, EUCLID_4:3;
hence ex a being Real st
( a <> 0 & x1 = a * x2 ) by A2; :: thesis: verum