len |.(<*> the carrier of F_Complex).| = len (<*> the carrier of F_Complex) by Def2
.= 0 ;
hence |.(<*> the carrier of F_Complex).| = <*> REAL ; :: thesis: verum