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