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