let V be RealLinearSpace; :: thesis: for f being Function of the carrier of V,REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V
let f be Function of the carrier of V,REAL; :: thesis: f (#) (<*> the carrier of V) = <*> the carrier of V
len (f (#) (<*> the carrier of V)) = len (<*> the carrier of V) by Def7
.= 0 ;
hence f (#) (<*> the carrier of V) = <*> the carrier of V ; :: thesis: verum