set f = AffineMap (a,0,c,0);
hereby TOPREAL9:def 4 AffineMap (a,0,c,0) is additive
let r be
Real;
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);
(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
;
verum
end;
let x, y be Point of (TOP-REAL 2); VECTSP_1:def 19 (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
; verum