let x be Element of REAL 0 ; :: thesis: x = <*> REAL
len x = 0 by FINSEQ_1:def 18;
hence x = <*> REAL ; :: thesis: verum