let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation holds
ex f' being Permutation of the carrier of (Lambda OAS) st
( f = f' & f' is_DIL_of Lambda OAS )
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation implies ex f' being Permutation of the carrier of (Lambda OAS) st
( f = f' & f' is_DIL_of Lambda OAS ) )
A1: Lambda OAS = AffinStruct(# the carrier of OAS,(lambda the CONGR of OAS) #) by DIRAF:def 2;
then reconsider f' = f as Permutation of the carrier of (Lambda OAS) ;
assume f is dilatation ; :: thesis: ex f' being Permutation of the carrier of (Lambda OAS) st
( f = f' & f' is_DIL_of Lambda OAS )
then A2: f is_FormalIz_of lambda the CONGR of OAS by Def8;
take f' ; :: thesis: ( f = f' & f' is_DIL_of Lambda OAS )
thus ( f = f' & f' is_DIL_of Lambda OAS ) by A2, A1, Def4; :: thesis: verum