let V be free Z_Module; :: thesis: for B being Basis of V
for u being Vector of V holds (Coordinate (u,B)) . (0. V) = 0
let B be Basis of V; :: thesis: for u being Vector of V holds (Coordinate (u,B)) . (0. V) = 0
let u be Vector of V; :: thesis: (Coordinate (u,B)) . (0. V) = 0
set f = Coordinate (u,B);
(Coordinate (u,B)) . (0. V) = (Coordinate (u,B)) . ((0. V) + (0. V))
.= ((Coordinate (u,B)) . (0. V)) + ((Coordinate (u,B)) . (0. V)) by defCoord ;
hence (Coordinate (u,B)) . (0. V) = 0 ; :: thesis: verum