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

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