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

ex f9 being Permutation of the carrier of (Lambda OAS) st

( f = f9 & f9 is_DIL_of Lambda OAS )

let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation implies ex f9 being Permutation of the carrier of (Lambda OAS) st

( f = f9 & f9 is_DIL_of Lambda OAS ) )

A1: Lambda OAS = AffinStruct(# the carrier of OAS,(lambda the CONGR of OAS) #) by DIRAF:def 2;

then reconsider f9 = f as Permutation of the carrier of (Lambda OAS) ;

assume f is dilatation ; :: thesis: ex f9 being Permutation of the carrier of (Lambda OAS) st

( f = f9 & f9 is_DIL_of Lambda OAS )

then A2: f is_FormalIz_of lambda the CONGR of OAS ;

take f9 ; :: thesis: ( f = f9 & f9 is_DIL_of Lambda OAS )

thus ( f = f9 & f9 is_DIL_of Lambda OAS ) by A2, A1; :: thesis: verum

ex f9 being Permutation of the carrier of (Lambda OAS) st

( f = f9 & f9 is_DIL_of Lambda OAS )

let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation implies ex f9 being Permutation of the carrier of (Lambda OAS) st

( f = f9 & f9 is_DIL_of Lambda OAS ) )

A1: Lambda OAS = AffinStruct(# the carrier of OAS,(lambda the CONGR of OAS) #) by DIRAF:def 2;

then reconsider f9 = f as Permutation of the carrier of (Lambda OAS) ;

assume f is dilatation ; :: thesis: ex f9 being Permutation of the carrier of (Lambda OAS) st

( f = f9 & f9 is_DIL_of Lambda OAS )

then A2: f is_FormalIz_of lambda the CONGR of OAS ;

take f9 ; :: thesis: ( f = f9 & f9 is_DIL_of Lambda OAS )

thus ( f = f9 & f9 is_DIL_of Lambda OAS ) by A2, A1; :: thesis: verum