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