let V be non empty CLSStruct ; :: thesis: for f being Function of the carrier of V,COMPLEX holds f (#) (<*> the carrier of V) = <*> the carrier of V
let f be Function of the carrier of V,COMPLEX; :: thesis: f (#) (<*> the carrier of V) = <*> the carrier of V
len (f (#) (<*> the carrier of V)) = len (<*> the carrier of V) by Def5
.= 0 ;
hence f (#) (<*> the carrier of V) = <*> the carrier of V ; :: thesis: verum