let x be Element of REAL 0 ; :: thesis: x = <*> REAL
len x = 0 by EUCLID:2;
hence x = <*> REAL ; :: thesis: verum