let OAS be OAffinSpace; :: thesis: id the carrier of OAS is dilatation

now

let x, y be Element of OAS; :: thesis: x,y '||' (id the carrier of OAS) . x,(id the carrier of OAS) . y
( (id the carrier of OAS) . x = x & (id the carrier of OAS) . y = y ) by FUNCT_1:18;
hence x,y '||' (id the carrier of OAS) . x,(id the carrier of OAS) . y by DIRAF:19; :: thesis: verum

end;

hence id the carrier of OAS is dilatation by Th51; :: thesis: verum