set h = incl (M2,M1);
the carrier of M2 c= the carrier of M1 by RMOD_2:def 2;
then A1: incl (M2,M1) = id the carrier of M2 by YELLOW_9:def 1;
thus incl (M2,M1) is additive :: thesis: incl (M2,M1) is scalar-linear
proof
let x, y be Element of M2; :: according to VECTSP_1:def 19 :: thesis: (incl (M2,M1)) . (x + y) = ((incl (M2,M1)) . x) + ((incl (M2,M1)) . y)
( (incl (M2,M1)) . x = x & (incl (M2,M1)) . y = y & (incl (M2,M1)) . (x + y) = x + y ) by A1, FUNCT_1:17;
hence (incl (M2,M1)) . (x + y) = ((incl (M2,M1)) . x) + ((incl (M2,M1)) . y) by RMOD_2:13; :: thesis: verum
end;
let x be Element of M2; :: according to FVALUAT1:def 16 :: thesis: for r being Element of R holds (incl (M2,M1)) . (x * r) = ((incl (M2,M1)) . x) * r
let r be Element of R; :: thesis: (incl (M2,M1)) . (x * r) = ((incl (M2,M1)) . x) * r
( (incl (M2,M1)) . x = x & (incl (M2,M1)) . (x * r) = x * r ) by A1, FUNCT_1:17;
hence (incl (M2,M1)) . (x * r) = ((incl (M2,M1)) . x) * r by RMOD_2:14; :: thesis: verum