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 number ; :: 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 ) by TOPREAL3:9;
A2: (r * x) `2 = r * (x `2 ) by TOPREAL3:9;
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, A2
.= r * |[((a * (x `1 )) + 0 ),((c * (x `2 )) + 0 )]| by EUCLID:62
.= 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 TOPREAL9:def 5 :: thesis: (AffineMap a,0 ,c,0 ) . (x + y) = ((AffineMap a,0 ,c,0 ) . x) + ((AffineMap a,0 ,c,0 ) . y)
A3: (x + y) `1 = (x `1 ) + (y `1 ) by TOPREAL3:7;
A4: (x + y) `2 = (x `2 ) + (y `2 ) by TOPREAL3:7;
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 A3, A4
.= |[((a * (x `1 )) + 0 ),((c * (x `2 )) + 0 )]| + |[(a * (y `1 )),(c * (y `2 ))]| by EUCLID:60
.= ((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