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