let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of (Lambda OAS) st f is_DIL_of Lambda OAS holds
ex f' being Permutation of the carrier of OAS st
( f = f' & f' is dilatation )
let f be Permutation of the carrier of (Lambda OAS); :: thesis: ( f is_DIL_of Lambda OAS implies ex f' being Permutation of the carrier of OAS st
( f = f' & f' is dilatation ) )
assume f is_DIL_of Lambda OAS ; :: thesis: ex f' being Permutation of the carrier of OAS st
( f = f' & f' is dilatation )
then A1: f is_FormalIz_of the CONGR of (Lambda OAS) by Def4;
A2: 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 OAS ;
take f' ; :: thesis: ( f = f' & f' is dilatation )
thus ( f = f' & f' is dilatation ) by A1, A2, Def8; :: thesis: verum