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

for x, y being Element of AFS holds x,y // (id the carrier of AFS) . x,(id the carrier of AFS) . y by AFF_1:2;

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

for x, y being Element of AFS holds x,y // (id the carrier of AFS) . x,(id the carrier of AFS) . y by AFF_1:2;

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