let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS holds

( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b )

let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b )

( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b )

let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b )

A1: now :: thesis: ( ( for a, b being Element of OAS holds a,b '||' f . a,f . b ) implies f is dilatation )

assume A2:
for a, b being Element of OAS holds a,b '||' f . a,f . b
; :: thesis: f is dilatation

for a, b being Element of OAS holds [[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS by A2, DIRAF:18;

then f is_FormalIz_of lambda the CONGR of OAS ;

hence f is dilatation ; :: thesis: verum

end;for a, b being Element of OAS holds [[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS by A2, DIRAF:18;

then f is_FormalIz_of lambda the CONGR of OAS ;

hence f is dilatation ; :: thesis: verum

now :: thesis: ( f is dilatation implies for a, b being Element of OAS holds a,b '||' f . a,f . b )

hence
( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b )
by A1; :: thesis: verumassume A3:
f is dilatation
; :: thesis: for a, b being Element of OAS holds a,b '||' f . a,f . b

let a, b be Element of OAS; :: thesis: a,b '||' f . a,f . b

f is_FormalIz_of lambda the CONGR of OAS by A3;

then [[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS ;

hence a,b '||' f . a,f . b by DIRAF:18; :: thesis: verum

end;let a, b be Element of OAS; :: thesis: a,b '||' f . a,f . b

f is_FormalIz_of lambda the CONGR of OAS by A3;

then [[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS ;

hence a,b '||' f . a,f . b by DIRAF:18; :: thesis: verum