set f = id G;

let a be Scalar of R; :: according to MOD_2:def 2 :: 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:18

.= a * ((id G) . x) by FUNCT_1:18 ; :: thesis: verum

let a be Scalar of R; :: according to MOD_2:def 2 :: 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:18

.= a * ((id G) . x) by FUNCT_1:18 ; :: thesis: verum