let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n st x1 // x2 & x2 // x3 holds
x1 // x3
let x1, x2, x3 be Element of REAL n; :: thesis: ( x1 // x2 & x2 // x3 implies x1 // x3 )
assume that
A1: x1 // x2 and
A2: x2 // x3 ; :: thesis: x1 // x3
A3: ex t being Real st x1 = t * x3
proof
consider b being Real such that
A4: x2 = b * x3 by A2;
consider a being Real such that
A5: x1 = a * x2 by A1;
x1 = (a * b) * x3 by A5, A4, EUCLID_4:4;
hence ex t being Real st x1 = t * x3 ; :: thesis: verum
end;
( x1 <> 0* n & x3 <> 0* n ) by A1, A2;
hence x1 // x3 by A3; :: thesis: verum