let AFS be AffinSpace; :: thesis: id the carrier of AFS is dilatation

now

let x, y be Element of AFS; :: thesis: x,y // (id the carrier of AFS) . x,(id the carrier of AFS) . y
( (id the carrier of AFS) . x = x & (id the carrier of AFS) . y = y ) by FUNCT_1:18;
hence x,y // (id the carrier of AFS) . x,(id the carrier of AFS) . y by AFF_1:2; :: thesis: verum

end;

hence id the carrier of AFS is dilatation by Th85; :: thesis: verum