set f = AffineMap (a,0,c,0);

hereby :: according to TOPREAL9:def 4 :: thesis: AffineMap (a,0,c,0) is additive

let r be Real; :: thesis: for x being Point of (TOP-REAL 2) holds (AffineMap (a,0,c,0)) . (r * x) = r * ((AffineMap (a,0,c,0)) . x)
let x be Point of (TOP-REAL 2); :: thesis: (AffineMap (a,0,c,0)) . (r * x) = r * ((AffineMap (a,0,c,0)) . x)
A1: ( (r * x) `1 = r * (x `1) & (r * x) `2 = r * (x `2) ) by TOPREAL3:4;
thus (AffineMap (a,0,c,0)) . (r * x) = |[((a * ((r * x) `1)) + 0),((c * ((r * x) `2)) + 0)]| by JGRAPH_2:def 2
.= |[(r * (a * (x `1))),(r * (c * (x `2)))]| by A1
.= r * |[((a * (x `1)) + 0),((c * (x `2)) + 0)]| by EUCLID:58
.= r * ((AffineMap (a,0,c,0)) . x) by JGRAPH_2:def 2 ; :: thesis: verum

end;

let x, y be Point of (TOP-REAL 2); :: according to VECTSP_1:def 19 :: thesis: (AffineMap (a,0,c,0)) . K326((TOP-REAL 2),x,y) = K326((TOP-REAL 2),((AffineMap (a,0,c,0)) . x),((AffineMap (a,0,c,0)) . y))
A2: ( (x + y) `1 = (x `1) + (y `1) & (x + y) `2 = (x `2) + (y `2) ) by TOPREAL3:2;
thus (AffineMap (a,0,c,0)) . (x + y) = |[((a * ((x + y) `1)) + 0),((c * ((x + y) `2)) + 0)]| by JGRAPH_2:def 2
.= |[((a * (x `1)) + (a * (y `1))),((c * (x `2)) + (c * (y `2)))]| by A2
.= |[((a * (x `1)) + 0),((c * (x `2)) + 0)]| + |[(a * (y `1)),(c * (y `2))]| by EUCLID:56
.= ((AffineMap (a,0,c,0)) . x) + |[((a * (y `1)) + 0),((c * (y `2)) + 0)]| by JGRAPH_2:def 2
.= ((AffineMap (a,0,c,0)) . x) + ((AffineMap (a,0,c,0)) . y) by JGRAPH_2:def 2 ; :: thesis: verum