thus id E is midpoints-preserving :: thesis: id E is Affine

proof

let a, b be Point of E; :: according to MAZURULM:def 3 :: thesis: (id E) . ((1 / 2) * (a + b)) = (1 / 2) * (((id E) . a) + ((id E) . b))
( (id E) . a = a & (id E) . b = b ) by FUNCT_1:18;
hence (id E) . ((1 / 2) * (a + b)) = (1 / 2) * (((id E) . a) + ((id E) . b)) by FUNCT_1:18; :: thesis: verum

end;

let a, b be Point of E; :: according to MAZURULM:def 2 :: thesis: for t being real number st 0 <= t & t <= 1 holds
(id E) . (((1 - t) * a) + (t * b)) = ((1 - t) * ((id E) . a)) + (t * ((id E) . b))
( (id E) . a = a & (id E) . b = b ) by FUNCT_1:18;
hence for t being real number st 0 <= t & t <= 1 holds
(id E) . (((1 - t) * a) + (t * b)) = ((1 - t) * ((id E) . a)) + (t * ((id E) . b)) by FUNCT_1:18; :: thesis: verum