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

f " is positive_dilatation

let f be Permutation of the carrier of OAS; :: thesis: ( f is positive_dilatation implies f " is positive_dilatation )

assume f is positive_dilatation ; :: thesis: f " is positive_dilatation

then A1: f is_DIL_of OAS ;

OAS is CongrSpace by Th26;

then f " is_DIL_of OAS by A1, Th24;

hence f " is positive_dilatation ; :: thesis: verum

f " is positive_dilatation

let f be Permutation of the carrier of OAS; :: thesis: ( f is positive_dilatation implies f " is positive_dilatation )

assume f is positive_dilatation ; :: thesis: f " is positive_dilatation

then A1: f is_DIL_of OAS ;

OAS is CongrSpace by Th26;

then f " is_DIL_of OAS by A1, Th24;

hence f " is positive_dilatation ; :: thesis: verum