let n be Element of 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 A2: ( x1 <> 0* n & x2 <> 0* n & ex r being Real st x1 = r * x2 ) by Def1;
consider a being Real such that
A3: x1 = a * x2 by A1, Def1;
a <> 0 by A2, A3, EUCLID_4:3;
hence ex a being Real st
( a <> 0 & x1 = a * x2 ) by A3; :: thesis: verum