let R be Ring; :: thesis: for G being LeftMod of R holds id G is linear
let G be LeftMod of R; :: thesis: id G is linear
set f = id G;

A1: now

let x, y be Vector of G; :: thesis: (id G) . (x + y) = ((id G) . x) + ((id G) . y)
( (id G) . (x + y) = x + y & (id G) . x = x ) by FUNCT_1:35;
hence (id G) . (x + y) = ((id G) . x) + ((id G) . y) by FUNCT_1:35; :: thesis: verum

end;

now

let a be Scalar of R; :: thesis: for x being Vector of G holds (id G) . (a * x) = a * ((id G) . x)
let x be Vector of G; :: thesis: (id G) . (a * x) = a * ((id G) . x)
thus (id G) . (a * x) = a * x by FUNCT_1:35
.= a * ((id G) . x) by FUNCT_1:35 ; :: thesis: verum

end;

hence id G is linear by A1, Def5; :: thesis: verum